Arrow Research search

Author name cluster

Michael Leuschel

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

19 papers
2 author rows

Possible papers

19

I&C Journal 2014 Journal Article

Fast offline partial evaluation of logic programs

  • Michael Leuschel
  • Germán Vidal

One of the most important challenges in partial evaluation is the design of automatic methods for ensuring the termination of the process. In this work, we introduce sufficient conditions for the strong (i. e. , independent of a computation rule) termination and quasi-termination of logic programs which rely on the construction of size-change graphs. We then present a fast binding-time analysis that takes the output of the termination analysis and annotates logic programs so that partial evaluation terminates. In contrast to previous approaches, the new binding-time analysis is conceptually simpler and considerably faster, scaling to medium-sized or even large examples.

Details DOI

I&C Journal 2012 Journal Article

Static slicing of explicitly synchronized languages

  • Michael Leuschel
  • Marisa Llorens
  • Javier Oliver
  • Josep Silva
  • Salvador Tamarit

Static analysis of concurrent languages is a complex task due to the non-deterministic execution of processes. If the concurrent language being studied allows process synchronization, then the analyses are even more complex (and thus expensive), e. g. , due to the phenomenon of deadlock. In this work we introduce a static analysis technique based on program slicing for concurrent and explicitly synchronized languages in general, and CSP in particular. Concretely, given a particular point in a specification, our technique allows us to know what parts of the specification must necessarily be executed before this point, and what parts of the specification could be executed before it. Our technique is based on a new data structure that extends the Synchronized Control Flow Graph (SCFG). We show that this new data structure improves the SCFG by taking into account the context in which processes are called and, thus, it makes the slicing process more precise. The technique has been implemented and tested with real specifications, producing good results. After formally defining our technique, we describe our tool, its architecture, its main applications and the results obtained from several experiments conducted in order to measure the performance of the tool.

Details DOI

LOPSTR Conference 2009 Conference Paper

Towards Just-In-Time Partial Evaluation of Prolog

  • Carl Friedrich Bolz
  • Michael Leuschel
  • Armin Rigo

Abstract We introduce a just-in-time specializer for Prolog. Just-in-time specialization attempts to unify of the concepts and benefits of partial evaluation (PE) and just-in-time (JIT) compilation. It is a variant of PE that occurs purely at runtime, which lazily generates residual code and is constantly driven by runtime feedback. Our prototype is an on-line just-in-time partial evaluator. A major focus of our work is to remove the overhead incurred when executing an interpreter written in Prolog. It improves over classical offline PE by requiring almost no heuristics nor hints from the author of the interpreter; it also avoids most termination issues due to interleaving execution and specialization. We evaluate the performance of our prototype on a small number of benchmarks.

Details

LOPSTR Conference 2008 Conference Paper

Fast Offline Partial Evaluation of Large Logic Programs

  • Michael Leuschel
  • Germán Vidal

Abstract In this paper, we present a fast binding-time analysis (BTA) by integrating a size-change analysis, which is independent of a selection rule, into a classical BTA for offline partial evaluation of logic programs. In contrast to previous approaches, the new BTA is conceptually simpler and considerably faster, scaling to medium-sized or even large examples and, moreover, it ensures both the so called local and global termination. We also show that through the use of selective hints, we can achieve both good specialisation results and a fast BTA and specialisation process.

Details

LOPSTR Conference 2008 Conference Paper

The MEB and CEB Static Analysis for CSP Specifications

  • Michael Leuschel
  • Marisa Llorens
  • Javier Oliver 0001
  • Josep Silva
  • Salvador Tamarit

Abstract This work presents a static analysis technique based on program slicing for CSP specifications. Given a particular event in a CSP specification, our technique allows us to know what parts of the specification must necessarily be executed before this event, and what parts of the specification could be executed before it in some execution. Our technique is based on a new data structure which extends the Synchronized Control Flow Graph (SCFG). We show that this new data structure improves the SCFG by taking into account the context in which processes are called and, thus, makes the slicing process more precise.

Details

LOPSTR Conference 2006 Conference Paper

Supervising Offline Partial Evaluation of Logic Programs Using Online Techniques

  • Michael Leuschel
  • Stephen-John Craig
  • Daniel Elphick

Abstract A major impediment for more widespread use of offline partial evaluation is the difficulty of obtaining and maintaining annotations for larger, realistic programs. Existing automatic binding-time analyses still only have limited applicability and annotations often have to be created or improved and maintained by hand, leading to errors. We present a technique to help overcome this problem by using online control techniques which supervise the specialisation process in order to detect such errors. We discuss an implementation in the logen system and show on a series of examples that this approach is effective: very few false alarms were raised while infinite loops were detected quickly. We also present the integration of this technique into a web interface, which highlights problematic annotations directly in the source code. A method to automatically fix incorrect annotations is presented, allowing the approach to be also used as a pragmatic binding time analysis. Finally we show how our method can be used for efficiently locating errors with built-ins inside Prolog source code.

Details

LOPSTR Conference 2004 Conference Paper

Fully Automatic Binding-Time Analysis for Prolog

  • Stephen-John Craig
  • John P. Gallagher
  • Michael Leuschel
  • Kim S. Henriksen

Abstract Offline partial evaluation techniques rely on an annotated version of the source program to control the specialisation process. These annotations guide the specialisation and ensure the termination of the partial evaluation. We present an algorithm for generating these annotations automatically. The algorithm uses state-of-the-art termination analysis techniques, combined with a new type-based abstract interpretation for propagating the binding types. This algorithm has been implemented as part of the logen partial evaluation system, along with a graphical annotation visualiser and editor, and we report on the performance of the algorithm for a series of benchmarks.

Details

LOPSTR Conference 2003 Invited Paper

Inductive Theorem Proving by Program Specialisation: Generating Proofs for Isabelle Using Ecce

  • Helko Lehmann
  • Michael Leuschel

Abstract In this paper we discuss the similarities between program specialisation and inductive theorem proving, and then show how program specialisation can be used to perform inductive theorem proving. We then study this relationship in more detail for a particular class of problems (verifying infinite state Petri nets) in order to establish a clear link between program specialisation and inductive theorem proving. In particular, we use the program specialiser ecce to generate specifications, hypotheses and proof scripts in the theory format of the proof assistant Isabelle. Then, in many cases, Isabelle can automatically execute these proof scripts and thereby verify the soundness of ecce ’s verification process and of the correspondence between program specialisation and inductive theorem proving.

Details

LOPSTR Conference 2001 Conference Paper

Abstract Conjunctive Partial Deduction Using Regular Types and Its Application to Model Checking

  • Michael Leuschel
  • Stefan Gruner

Abstract We present an abstract partial deduction technique which uses regular types as its domain and which can handle conjunctions, and thus perform deforestation and tupling. We provide a detailed description of all the required operations and present an implementation within the ecce system. We discuss the power of this new specialisation algorithm, especially in the light of verifying and specialising infinite state process algebras. Here, our new algorithm can provide a more precise treatment of synchronisation and can be used for refinement checking.

Details

LOPSTR Conference 2000 Conference Paper

Infinite State Model Checking by Abstract Interpretation and Program Specialisation

  • Michael Leuschel
  • Thierry Massart

Abstract We illustrate the use of logic programming techniques for finite model checking of CTL formulae. We present a technique for infinite state model checking of safety properties based upon logic program specialisation and analysis techniques. The power of the approach is illustrated on several examples. For that, the efficient tools logen and ecce are used. We discuss how this approach has to be extended to handle more complicated infinite state systems and to handle arbitrary CTL formulae.

Details

LPAR Conference 2000 Conference Paper

Solving Planning Problems by Partial Deduction

  • Helko Lehmann
  • Michael Leuschel

Abstract We develop an abstract partial deduction method capable of solving planning problems in the Fluent Calculus. To this end, we extend “classical” partial deduction to accommodate both, equational theories and regular type information. We show that our new method is actually complete for conjunctive planning problems in the propositional Fluent Calculus. Furthermore, we believe that our approach can also be used for more complex systems, e. g. , in cases where completeness can not be guaranteed due to general undecidability.

Details

LOPSTR Conference 1998 Conference Paper

Preserving Termination of Tabled Logic Programs While Unfolding

  • Michael Leuschel
  • Bern Martens
  • Konstantinos Sagonas

Abstract We provide a first investigation of the specialisation and transformation of tabled logic programs through unfolding. We show that — surprisingly — unfolding, even determinate, can worsen the termination behaviour in the context of tabling. We therefore establish two criteria which ensure that such mishaps are avoided. We also briefly discuss the influence of some other transformation techniques on the termination and efficiency of tabled logic programs.

Details

LOPSTR Conference 1998 Conference Paper

Termination Analysis for Tabled Logic Programming

  • Stefaan Decorte
  • Danny De Schreye
  • Michael Leuschel
  • Bern Martens
  • Konstantinos Sagonas

Abstract We provide a theoretical basis for studying the termination of tabled logic programs executed under SLG-resolution using a left-to-right computation rule. To this end, we study the classes of quasi-terminating and LG-terminating programs (for a set of atomic goals S ). These are tabled logic programs where execution of each call from S leads to only a finite number of different (i. e. , non-variant) calls, and a finite number of different calls and computed answer substitutions for them, respectively. We then relate these two classes through a program transformation, and present a characterisation of quasi-termination by means of the notion of quasi-acceptability of tabled programs. The latter provides us with a practical method of proving termination and the method is illustrated on non-trivial examples of tabled logic programs.

Details

LOPSTR Conference 1997 Conference Paper

Conjunctive Partial Deduction in Practice

  • Jesper Jørgensen
  • Michael Leuschel
  • Bern Martens

Abstract Recently, partial deduction of logic programs has been extended to conceptually embed folding. To this end, partial deductions are no longer computed of single atoms, but rather of entire conjunctions; Hence the term “conjunctive partial deduction”. Conjunctive partial deduction aims at achieving unfold/fold-like program transformations such as tupling and deforestation within fully automated partial deduction. However, its merits greatly surpass that limited context: Also other major efficiency gains can be obtained through considerably improved side-ways information propagation. In this paper, we present a first investigation of conjunctive partial deduction in practice. We describe the concrete options used in the implementation(s), look at abstraction in a practical Prolog context, include and discuss an extensive set of benchmark results. ¿ From these, we can conclude that conjunctive partial deduction can indeed pay off in practice, beating its conventional precursor on a number of small to medium size programs. However, controlling it in a perfect way proves far from obvious, and a range of challenging open problems remain as topics for further research.

Details

LOPSTR Conference 1997 Conference Paper

Logic Program Specialisation: How to Be More Specific (Abstract)

  • Michael Leuschel
  • Danny De Schreye

Abstract Standard partial deduction suffers from several drawbacks when compared to top-down abstract interpretation schemes. Conjunctive partial deduction, an extension of standard partial deduction, remedies one of those, namely the lack of side-ways information passing. But two other problems remain: the lack of success-propagation as well as the lack of inference of global success-information. We illustrate these drawbacks and show how they can be remedied by combining conjunctive partial deduction with an abstract interpretation technique known as more specific program construction. We present a simple, as well as a more refined integration of these methods. Finally we illustrate the practical relevance of this approach for some advanced applications, where it surpasses the precision of current abstract interpretation techniques.

Details

LOPSTR Conference 1997 Conference Paper

Redundant Argument Filtering of Logic Programs

  • Michael Leuschel
  • Morten Heine Sørensen

Abstract This paper is concerned with the problem of removing redundant arguments from logic programs. Such arguments can be removed without affecting correctness, in a certain sense. Most program specialisation techniques, even though they filter arguments and remove clauses, fail to remove a substantial number of redundant arguments, yielding in some cases rather inefficient residual programs. We formalise the notion of a redundant argument and show that one cannot effectively remove all redundant arguments. We then give a safe, effective approximation of the notion of a redundant argument and describe several simple and efficient algorithms based on the approximative notion. We conduct extensive experiments with our algorithms on mechanically generated programs illustrating the practical benefits of our approach.

Details

LOPSTR Conference 1996 Conference Paper

Ecological Partial Deduction: Preserving Characteristic Trees Without Constraints

  • Michael Leuschel

Abstract A partial deduction strategy for logic programs usually uses an abstraction operation to guarantee the finiteness of the set of atoms for which partial deductions are produced. Finding an abstraction operation which guarantees finiteness and does not loose relevant information is a difficult problem. In earlier work Gallagher and Bruynooghe proposed to base the abstraction operation on characteristic paths and trees. A characteristic tree captures the relevant structure of the generated partial SLDNF-tree for a given goal. Unfortunately the abstraction operations proposed in the earlier work do not always produce more general atoms and do not always preserve the characteristic trees. This problem has been solved for purely determinate unfolding rules and definite programs in [12, 13] by using constraints inside the partial deduction process. In this paper we propose an alternate solution which achieves the preservation of characteristic trees for any unfolding rule, normal logic programs (it can even handle some built-in's if so desired) and without adding constraints to the partial deduction process (making the re-use of existing unfolding techniques very simple). We thus provide a powerful, generally applicable and elegant abstraction operation for partial deduction providing a fine-grained and terminating control of polyvariance.

Details

LOPSTR Conference 1994 Conference Paper

Partial Evaluation of the "Real Thing"

  • Michael Leuschel

Abstract In this paper we present a partial evaluation scheme for a “real life” subset of Prolog. This subset contains first-order built-in's, simple side-effects and the operational predicate if-then-else. We outline a denotational semantics for this subset of Prolog and show how partial deduction can be extended to specialise programs of this kind. We point out some of the problems not occurring in partial deduction and show how they can be solved in our setting. Finally we provide some results based on an implementation of the above.

Details

LOPSTR Conference 1990 Conference Paper

Improving Homeomorphic Embedding for Online Termination

  • Michael Leuschel

Abstract Well-quasi orders in general, and homeomorphic embedding in particular, have gained popularity to ensure online termination of program analysis, specialisation and transformation techniques. It has been recently shown that the homeomorphic embedding relation is strictly more powerful than a large class of involved well-founded approaches. In this paper we provide some additional investigations on the power of homeomorphic embedding. We, however, also illustrate that the homeomorphic embedding relation suffers from several inadequacies in contexts where logical variables arise. We therefore present new, extended homeomorphic embedding relations to remedy this problem.

Details
v2026.09.13