Jens Bendisposto, Michael Jastram, Michael Leuschel, Christian Lochert, Björn Scheuermann, Ingo Weigelt
Replace this file with prentcsmacro.sty for your meeting,
Improving Size-Change Analysis in Offline Partial Evaluation (2009)
Leuschel, Michael, Tamarit, Salvador, Vidal, German
Some recent approaches for scalable offline partial evaluation of logic programs include a size-change analysis for ensuring both so called local and global termination. In this work|inspired by...
A Semantics-Aware Editing Environment for Prolog in Eclipse (2009)
Bendisposto, Jens, Endrijautzki, Ian, Leuschel, Michael, Schneider, David
In this paper we present a Prolog plugin for Eclipse based upon BE4, and providing many features such as semantic-aware syntax highlighting, outline view, error marking, content assist, hover...
logic and constraint programming (2008)
Steve Barker, Michael Leuschel, Mauricio Varea
We describe the use of a flexible meta-interpreter for performing access control checks on deductive databases. The meta-program is implemented in Prolog and takes as input a database and an access...
Michael Leuschel, Michael Butler
Abstract. We present ProB, an animation and model checking tool for the B method. ProB’s animation facilities allow users to gain confidence in their specifications, and unlike the animator...
LTL Model Checking of CSP by Refinement or How to Make FDR Spin (2008)
Andrew Currie, Michael Leuschel, Thierry Massart
Abstract. We present evidence that the refinement-based approach to verification does not seem to be very well suited for verifying temporal properties of a system. We then show how to (and how not...
A flexible Prolog Interpreter in Python (2008)
Carl Friedrich Bolz, Michael Leuschel, Lehrstuhl Softwaretechnik
Abstract. We provide a proof-of-concept for a new approach to flexible and portable implementation of programming languages. More precisely, we describe the implementation of a Prolog interpreter in...
Michael Leuschel, Stephen-john Craig
We present ECCE and LOGEN, two partial evaluators for Prolog using the online and offline approach respectively. We briefly present the foundations of these tools and discuss various applications. We...
The Use of Formal Methods in the Analysis of Trust (Position Paper) (2008)
Michael Butler, Michael Leuschel, Stéphane Lo Presti, Phillip Turner
Abstract. Security and trust are two properties of modern computing systems that are the focus of much recent interest. They play an increasingly significant role in the requirements for modern...
Michael Leuschel, Maurice Bruynooghe
Program specialisation aims at improving the overall performance of programs by performing source to source transformations. A common approach within functional and logic programming, known...
Steve Barker, Michael Leuschel, Mauricio Varea
We describe the use of a flexible meta-interpreter for performing access control checks on deductive databases. The meta-program is implemented in Prolog and takes as input a database and an access...
Automatic Testing from Formal Specifications ⋆ (2008)
Manoranjan Satpathy, Michael Butler, Michael Leuschel, S. Ramesh
Abstract. In this article, we consider model oriented formal specification languages. We generate test cases by performing symbolic execution over a model, and from the test cases obtain a Java...
Tools for system validation with B abstract machines (2008)
Michael Butler, Michael Leuschel, Colin Snook
Abstract. In this paper we give an overview of some tools that we have developed to support the application of the B Method. ProB is an animation and model checking tool for the B method. ProB’s...
Model Checking Object Petri Nets in Maude and Prolog (2008)
Berndt Farwer, Michael Leuschel
Object Petri nets (OPNs) provide a natural and modular method for modelling many realworld systems. We give a structure-preserving translation of OPNs to Prolog by encoding the OPN semantics,...
Symmetry reduced model checking for B (2008)
Edd Turner, Michael Leuschel, Corinna Spermann, Michael Butler
Symmetry reduction is a technique that can help alleviate the problem of state space explosion in model checking. The idea is to verify only a subset of states from each class (orbit) of symmetric...
Efficient Approximate Verification of Promela Models via Symmetry Markers (2008)
Alastair F. Donaldson, Michael Leuschel
Abstract. We present a new verification technique for Promela which exploits state-space symmetries induced by scalarset values used in a model. The technique involves efficiently computing a marker...
Stephen-john Craig, Michael Leuschel
Abstract. The Lloyd-Topor transformation is a classical transformation that translates extended logic programs with logical connectives and explicit quantifiers into normal logic programs. In this...
Efficient Approximate Verification of Promela Models via Symmetry Markers (2008)
Alastair F. Donaldson, Michael Leuschel
Abstract. We present a new verification technique for Promela which exploits state-space symmetries induced by scalarset values used in a model. The technique involves efficiently computing a marker...
Michael Leuschel, Stephen-john Craig
We present ECCE and LOGEN, two partial evaluators for Prolog using the online and offline approach respectively. We briefly present the foundations of these tools and discuss various applications. We...
logic and constraint programming (2008)
Steve Barker, Michael Leuschel, Mauricio Varea
We describe the use of a flexible meta-interpreter for performing access control checks on deductive databases. The meta-program is implemented in Prolog and takes as input a database and an access...
Inductive Theorem Proving by Program Specialisation: Generating proofs for (2008)
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...
Program Specialisation as a Preprocessing Step for Termination Analysis (2008)
Manh Thang Nguyen, Maurice Bruynooghe, Danny De Schreye, Michael Leuschel
Previous works have shown that the structure information of a logic program can be used to transform it to another program such that the transformation is termination preserving and termination proof...
Logic programming originated from the discovery that a subset of predicate logic could be given a procedural interpretation which was first embodied in the programming language Prolog. The unique...
Tools for system validation with B (2008)
Machines Michael Butler, Michael Butler, Michael Leuschel, Colin Snook
In this paper we give an overview of some tools that we have developed to support the application of the B Method. ProB is an animation and model checking tool for the B method. ProB's animation...
ProB: An Automated Analysis Toolset for the B Method (2008)
Leuschel, Michael, Butler, Michael
We present ProB, a validation toolset for the B method. ProB's automated animation facilities allow users to gain confidence in their specifications. ProB also contains a model checker and a...
ProB: An Automated Analysis Toolset for the B Method (2008)
Leuschel, Michael, Butler, Michael
We present ProB, a validation toolset for the B method. ProB's automated animation facilities allow users to gain confidence in their specifications. ProB also contains a model checker and a...
Advanced Techniques for (2007)
Logic Program Specialisation, Michael Leuschel
Program specialisation, also called partial evaluation or partial deduction, is an automatic technique for program optimisation. The central idea is to specialise a given source program for a...
Michael Leuschel, Maurice Bruynooghe
Program specialisation aims at improving the overall performance of programs by performing source to source transformations. A common approach within functional and logic programming, known...
Michael Leuschel, Ivan Wolton, Thierry Massart, Laksono Adhianto
Abstract. We study the possibility of doing LTL model checking on CSP specications in the context of renement. We present a technique to perform LTL model checking of CSP processes using renement...
Michael Leuschel, Jesper Jrgensen, Wim Vanhoof, Maurice Bruynooghe
The so called "cogen approach " to program specialisation, writing a compiler generator instead of a specialiser, has been used with considerable success in partial evaluation of...
Finite and Infinite Model Checking of Dual Transition Petri Net Models (2007)
Mauricio Varea, Bashir Al-hashimi, Michael Leuschel
The formal verification of embedded systems is becoming a key research area due to the ever increasing design complexity involved in the modelling and validation of embedded systems. Traditional...
Danny De Schreye, Robert Gl Uck, Michael Leuschel, Bern Martens, Heine Srensen
. Partial deduction in the Lloyd-Shepherdson framework cannot achieve certain optimisations which are possible by unfold/fold transformations. We introduce conjunctive partial deduction, an extension...
Some Results and Open Issues (2007)
Konstantinos Sagonas, Konstantinos Sagonas, Michael Leuschel, Michael Leuschel
personal or classroom use is granted without fee provided that the copies are not made or distributed for profit or commercial advantage, the copyright notice, the title of the publication, and its...
. Integrity constraints are useful for the specification of deductive databases, as well as for inductive and abductive logic programs. Verifying integrity constraints upon updates is a major...
Danny De Schreye, Robert Gl Uck, Michael Leuschel, Bern Martens, Heine Srensen
. Partial deduction in the Lloyd-Shepherdson framework cannot achieve certain optimisations which are possible by unfold/fold transformations. We introduce conjunctive partial deduction, an extension...
Infinite State Model Checking using Partial Evaluation and Abstract Interpretation (2007)
Logic programming originated from the discovery that a subset of predicate logic could be given a procedural interpretation which was first embodied in the programming language Prolog. The unique...
Infinite State Model Checking Using Partial Evaluation and Abstract Interpretation (2007)
Interpretation Final Report for GR/N11667/01 (Accompanies Individual Grant Review Form) Michael Leuschel, University of Southampton 1 Background/Context Logic programming originated from the...
Symmetry Reduced Model Checking for B (2007)
Turner, Edd, Leuschel, Michael, Spermann, Corinna, Butler, Michael
Symmetry reduction is a technique that can help alleviate the problem of state space explosion in model checking. The idea is to verify only a subset of states from each class (orbit) of symmetric...
Symmetry Reduced Model Checking for B (2007)
Turner, Edd, Leuschel, Michael, Spermann, Corinna, Butler, Michael
Symmetry reduction is a technique that can help alleviate the problem of state space explosion in model checking. The idea is to verify only a subset of states from each class (orbit) of symmetric...
Symmetry Reduced Model Checking for B (2007)
Turner, Edd, Leuschel, Michael, Spermann, Corinna, Butler, Michael
Symmetry reduction is a technique that can help alleviate the problem of state space explosion in model checking. The idea is to verify only a subset of states from each class (orbit) of symmetric...
Symmetry Reduced Model Checking for B (2007)
Turner, Edd, Leuschel, Michael, Spermann, Corinna, Butler, Michael
Symmetry reduction is a technique that can help alleviate the problem of state space explosion in model checking. The idea is to verify only a subset of states from each class (orbit) of symmetric...
Symmetry Reduction for B by Permutation Flooding (2007)
Leuschel, Michael, Butler, Michael, Spermann, Corinna, Turner, Edd
Symmetry Reduced Model Checking for B (2007)
Turner, Edd, Leuschel, Michael, Spermann, Corinna, Butler, Michael
Symmetry reduction is a technique that can help alleviate the problem of state space explosion in model checking. The idea is to verify only a subset of states from each class (orbit) of symmetric...
Symmetry Reduced Model Checking for B (2007)
Turner, Edd, Leuschel, Michael, Spermann, Corinna, Butler, Michael
Symmetry reduction is a technique that can help alleviate the problem of state space explosion in model checking. The idea is to verify only a subset of states from each class (orbit) of symmetric...
Automatic Testing from Formal Specifications (2007)
Satpathy, Manoranjan, Butler, Michael, Leuschel, Michael, Ramesh, S
Symmetry Reduction for B by Permutation Flooding (2007)
Leuschel, Michael, Butler, Michael, Spermann, Corinna, Turner, Edd
Automatic Testing from Formal Specifications (2007)
Satpathy, Manoranjan, Butler, Michael, Leuschel, Michael, Ramesh, S
Michael Leuschel, Michael Butler
Abstract. We present ProB, a validation toolset for the B method. ProB’s automated animation facilities allow users to gain confidence in their specifications. ProB also contains a model checker...
Michael Leuschel, Michael Butler
Abstract. We present ProB, a validation toolset for the B method. ProB’s automated animation facilities allow users to gain confidence in their specifications. ProB also contains a model checker...
A Prolog Interpreter in Python (2007)
Carl Friedrich Bolz, Gutachter Prof, Dr. Michael Leuschel, Prof Dr, Stefan Conrad, ...
We provide a proof-of-concept for a new approach to flexible and portable implementation of programming languages. More precisely, we describe the implementation of a Prolog interpreter in RPython, a...
Validating Z Specifications using the ProB Animator and Model Checker (2007)
Daniel Plagge, Michael Leuschel
Abstract. We present the architecture and implementation of the proz tool to validate high-level Z specifications. The tool was integrated into prob, by providing a translation of Z into B and by...
A Generic Flash-Based Animation Engine for ProB (2007)
Jens Bendisposto, Michael Leuschel
Abstract. Writing a formal specification for real-life, industrial problems is a difficult and error prone task, even for experts in formal methods. In the process of specifying a formal model for...
Automatic Testing from Formal Specifications (2006)
Satpathy, Manoranjan, Butler, Michael, Ramesh, Sethu, Leuschel, Michael
In this article, we consider model oriented formal specification languages. We generate test cases by performing symbolic execution over a model, and from the test cases obtain a Java program. This...
ProB: An Automated Analysis Toolset for the B Method (2006)
Leuschel, Michael, Butler, Michael
We present ProB, a validation toolset for the B method. ProB's automated animation facilities allow users to gain confidence in their specifications. ProB also contains a model checker and a...
Symmetry Reduction for B by Permutation Flooding (2006)
Leuschel, Michael, Butler, Michael, Spermann, Corinna, Turner, Edd
Symmetry Reduction for B by Permutation Flooding (2006)
Leuschel, Michael, Butler, Michael, Spermann, Corinna, Turner, Edd
Symmetry Reduction for B by Permutation Flooding (2006)
Leuschel, Michael, Butler, Michael, Spermann, Corinna, Turner, Edd
Holistic Trust Design of E-Services (2006)
Lo Presti, Stéphane, Butler, Michael, Leuschel, Michael, Booth, Chris
Efficient and Flexible Access Control via Jones-Optimal Logic Program Specialisation (2006)
Barker, Steve, Leuschel, Michael, Varea, Mauricio
We describe the use of a flexible meta-interpreter for performing access control checks on deductive databases. The meta-program is implemented in Prolog and takes as input a database and an access...
Supervising Offline Partial Evaluation of Logic Programs using Online Techniques (2006)
Leuschel, Michael, Craig, Stephen-John, Elphick, Dan
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...
The Ecce and Logen Partial Evaluators and their Web Interfaces (2006)
Leuschel, Michael, Elphick, Dan, Varea, Mauricio, Craig, Stephen-John, Fontaine, Marc
We present Ecce and Logen, two partial evaluators for Prolog using the online and offline approach respectively. We briefly present the foundations of these tools and discuss various applications. We...
Holistic Trust Design of E-Services (2006)
Lo Presti, Stéphane, Butler, Michael, Leuschel, Michael, Booth, Chris
Efficient and Flexible Access Control via Jones-Optimal Logic Program Specialisation (2006)
Barker, Steve, Leuschel, Michael, Varea, Mauricio
We describe the use of a flexible meta-interpreter for performing access control checks on deductive databases. The meta-program is implemented in Prolog and takes as input a database and an access...
Supervising Offline Partial Evaluation of Logic Programs using Online Techniques (2006)
Leuschel, Michael, Craig, Stephen-John, Elphick, Dan
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...
The Ecce and Logen Partial Evaluators and their Web Interfaces (2006)
Leuschel, Michael, Elphick, Dan, Varea, Mauricio, Craig, Stephen-John, Fontaine, Marc
We present Ecce and Logen, two partial evaluators for Prolog using the online and offline approach respectively. We briefly present the foundations of these tools and discuss various applications. We...
Holistic Trust Design of E-Services (2006)
Lo Presti, Stéphane, Butler, Michael, Leuschel, Michael, Booth, Chris
Efficient and Flexible Access Control via Jones-Optimal Logic Program Specialisation (2006)
Barker, Steve, Leuschel, Michael, Varea, Mauricio
We describe the use of a flexible meta-interpreter for performing access control checks on deductive databases. The meta-program is implemented in Prolog and takes as input a database and an access...
Supervising Offline Partial Evaluation of Logic Programs using Online Techniques (2006)
Leuschel, Michael, Craig, Stephen-John, Elphick, Dan
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...
The Ecce and Logen Partial Evaluators and their Web Interfaces (2006)
Leuschel, Michael, Elphick, Dan, Varea, Mauricio, Craig, Stephen-John, Fontaine, Marc
We present Ecce and Logen, two partial evaluators for Prolog using the online and offline approach respectively. We briefly present the foundations of these tools and discuss various applications. We...
Supervising Offline Partial Evaluation of Logic Programs using Online Techniques (2006)
Michael Leuschel, Stephen-john Craig, Dan 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...
Susana Muñoz Hernández, Susana Muñoz Hernández, Maria Alpuente, Mireille Ducasse, Moreno Falaschi, ...
There were 12 submissions. Each submission was reviewed by at least 3 programme committee members. The committee decided to accept 9 papers for presentation at the workshop. The workshop organisers...
Automatic Testing from Formal Specifications (2006)
Michael Leuschel, Manoranjan Satpathy, Michael Butler, S. Ramesh, Michael Leuschel
In this article, we consider model oriented formal specification languages. We generate test cases by performing symbolic execution over a model, and from the test cases obtain a Java program. This...
Supervising Offline Partial Evaluation of Logic Programs using Online Techniques (2006)
Michael Leuschel, Stephen-john Craig, Dan 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...
Integration of the ProB model checker into Eclipse (2006)
Softwaretechnik Und Programmiersprachen, Jens Marco Bendisposto, Gutachter Prof, Dr. Michael Leuschel, Prof Dr, Stefan Conrad, ...
Hiermit versichere ich, dass ich diese Bachelorarbeit selbstständig verfasst habe. Ich habe dazu keine anderen als die angegebenen Quellen und Hilfsmittel verwendet.
Daniel Jackson and Pamela Zave, Editors ISBN 1-59593-584-3 Programme Chairs (2006)
Daniel Jackson, Pamela Zave, Pamela Zave, T Laboratories, Martin Gogolla, Shriram Krishnamurthi, ...
Alloy is one of several emerging ‘lightweight formal methods ’ that use simple first-order logics for expressing designs and properties, coupled with constraint solving technology for automatic...
Michael Leuschel, Dominique Cansell, Michael Butler, Loria Nancy
Abstract. ProB is an animation and model checking tool for the B Method, which can deal with many interesting specifications. Some specifications, however, contain complicated functions which cannot...
Efficient and flexible access control via jones optimality logic program specialisation (2006)
Steve Barker, Michael Leuschel, Mauricio Varea
Abstract. We describe the use of a flexible meta-interpreter for performing access control checks on deductive databases. The meta-program is implemented in Prolog and takes as input a database and...
Efficient and flexible access control via jones optimality logic program specialisation (2006)
Steve Barker, Michael Leuschel, Mauricio Varea
Abstract. We describe the use of a flexible meta-interpreter for performing access control checks on deductive databases. The meta-program is implemented in Prolog and takes as input a database and...
Animating and Model Checking B Specifications with Higher-Order Recursive Functions (2006)
Leuschel, Michael, Bendisposto, Jens
Real-life specifications often contain complicated functions. Animation and validation of such functions and specifications is very important. However, such functions pose a major challenge to...
Visualising Larger State Spaces in ProB (2005)
ProB is an animator and model checker for the B method. It also allows to visualise the state space of a B machine in graphical way. This is often very useful and allows users to quickly spot whether...
Visualising Larger State Spaces in ProB (2005)
ProB is an animator and model checker for the B method. It also allows to visualise the state space of a B machine in graphical way. This is often very useful and allows users to quickly spot whether...
Visualising Larger State Spaces in ProB (2005)
ProB is an animator and model checker for the B method. It also allows to visualise the state space of a B machine in graphical way. This is often very useful and allows users to quickly spot whether...
ProTest: An Automatic Test Environment for B Specifications (2005)
Satpathy, Manoranjan, Leuschel, Michael, Butler, Michael
We present ProTest, an automatic test environment for B specifications. B is a model-oriented notation where systems are specified in terms of abstract states and operations on abstract states....
Tools for system validation with B abstract machines (2005)
Butler, Michael, Leuschel, Michael, Snook, Colin
In this paper we give an overview of some tools that we have developed to support the application of the B Method. ProB is an animation and model checking tool for the B method. ProB's animation...
Forward Slicing by Conjunctive Partial Deduction and Argument Filtering (2005)
Leuschel, Michael, Vidal, German
Program slicing is a well-known methodology that aims at identifying the program statements that (potentially) affect the values computed at some point of interest. Within imperative programming,...
Towards Provably Correct Code Generation via Horn Logical Continuation Semantics (2005)
Wang, Qian, Gupta, Gopal, Leuschel, Michael
Provably correct compilation is an important aspect in development of high assurance software systems. In this paper we explore approaches to provably correct code generation based on programming...
Self-Tuning Resource Aware Specialisation for Prolog (2005)
Craig, Stephen-John, Leuschel, Michael
The paper develops a self-tuning resource aware partial evaluation technique for Prolog programs, which derives its own control strategies tuned for the underlying computer architecture and Prolog...
A Reconstruction of the Lloyd-Topor Transformation using Partial Evaluation (2005)
Leuschel, Michael, Craig, Stephen-John
The Lloyd-Topor transformation is a classical transformation that translates extended logic programs with logical connectives and explicit quantifiers into normal logic programs. In this paper we...
Automatic Refinement Checking for B (2005)
Leuschel, Michael, Butler, Michael
Refinement is a key concept in the B-Method. While refinement is at the heart of the B Method, so far no automatic refinement checker has been developed for it. In this paper we present a refinement...
ProTest: An Automatic Test Environment for B Specifications (2005)
Satpathy, Manoranjan, Leuschel, Michael, Butler, Michael
We present ProTest, an automatic test environment for B specifications. B is a model-oriented notation where systems are specified in terms of abstract states and operations on abstract states....
ProTest: An Automatic Test Environment for B Specifications (2005)
Satpathy, Manoranjan, Leuschel, Michael, Butler, Michael
We present ProTest, an automatic test environment for B specifications. B is a model-oriented notation where systems are specified in terms of abstract states and operations on abstract states....
Tools for system validation with B abstract machines (2005)
Butler, Michael, Leuschel, Michael, Snook, Colin
In this paper we give an overview of some tools that we have developed to support the application of the B Method. ProB is an animation and model checking tool for the B method. ProB's animation...
Forward Slicing by Conjunctive Partial Deduction and Argument Filtering (2005)
Leuschel, Michael, Vidal, German
Program slicing is a well-known methodology that aims at identifying the program statements that (potentially) affect the values computed at some point of interest. Within imperative programming,...
Towards Provably Correct Code Generation via Horn Logical Continuation Semantics (2005)
Wang, Qian, Gupta, Gopal, Leuschel, Michael
Provably correct compilation is an important aspect in development of high assurance software systems. In this paper we explore approaches to provably correct code generation based on programming...
Self-Tuning Resource Aware Specialisation for Prolog (2005)
Craig, Stephen-John, Leuschel, Michael
The paper develops a self-tuning resource aware partial evaluation technique for Prolog programs, which derives its own control strategies tuned for the underlying computer architecture and Prolog...
A Reconstruction of the Lloyd-Topor Transformation using Partial Evaluation (2005)
Leuschel, Michael, Craig, Stephen-John
The Lloyd-Topor transformation is a classical transformation that translates extended logic programs with logical connectives and explicit quantifiers into normal logic programs. In this paper we...
Automatic Refinement Checking for B (2005)
Leuschel, Michael, Butler, Michael
Refinement is a key concept in the B-Method. While refinement is at the heart of the B Method, so far no automatic refinement checker has been developed for it. In this paper we present a refinement...
Fully Automatic Binding Time Analysis for Prolog (2005)
Craig, Stephen, Gallagher, John Patrick, Leuschel, Michael, Henriksen, Kim Steen
Fully Automatic Binding Time Analysis for Prolog (2005)
Craig, Stephen, Gallagher, John Patrick, Leuschel, Michael, Henriksen, Kim Steen
Tools for system validation with B abstract machines (2005)
Butler, Michael, Leuschel, Michael, Snook, Colin
In this paper we give an overview of some tools that we have developed to support the application of the B Method. ProB is an animation and model checking tool for the B method. ProB's animation...
Forward Slicing by Conjunctive Partial Deduction and Argument Filtering (2005)
Leuschel, Michael, Vidal, German
Program slicing is a well-known methodology that aims at identifying the program statements that (potentially) affect the values computed at some point of interest. Within imperative programming,...
Towards Provably Correct Code Generation via Horn Logical Continuation Semantics (2005)
Wang, Qian, Gupta, Gopal, Leuschel, Michael
Provably correct compilation is an important aspect in development of high assurance software systems. In this paper we explore approaches to provably correct code generation based on programming...
Self-Tuning Resource Aware Specialisation for Prolog (2005)
Craig, Stephen-John, Leuschel, Michael
The paper develops a self-tuning resource aware partial evaluation technique for Prolog programs, which derives its own control strategies tuned for the underlying computer architecture and Prolog...
A Reconstruction of the Lloyd-Topor Transformation using Partial Evaluation (2005)
Leuschel, Michael, Craig, Stephen-John
The Lloyd-Topor transformation is a classical transformation that translates extended logic programs with logical connectives and explicit quantifiers into normal logic programs. In this paper we...
Automatic Refinement Checking for B (2005)
Leuschel, Michael, Butler, Michael
Refinement is a key concept in the B-Method. While refinement is at the heart of the B Method, so far no automatic refinement checker has been developed for it. In this paper we present a refinement...
Fully Automatic Binding Time Analysis for Prolog (2005)
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 have to ensure...
Automatic refinement checking for B (2005)
Michael Leuschel, Michael Butler
Abstract. While refinement is at the heart of the B Method, so far no automatic refinement checker has been developed for it. In this paper we present a refinement checking algorithm and...
Combining CSP and B for Specification and Property Verification (2005)
Michael Butler, Michael Leuschel
Abstract. ProB is a model checking tool for the B Method. In this paper we present an extension of ProB that supports checking of specifications written in a combination of CSP and B. We explain how...
Automatic refinement checking for B (2005)
Michael Leuschel, Michael Butler
Abstract. While refinement is at the heart of the B Method so far no automatic refinement checker has been developed for it. In this paper we present a refinement checking algorithm and...
Forward Slicing by Conjunctive Partial Deduction and Argument Filtering (2005)
Michael Leuschel, Germán Vidal
Abstract. Program slicing is a well-known methodology that aims at identifying the program statements that (potentially) affect the values computed at some point of interest. Within imperative...
Towards provably correct code generation via horn logical continuation semantics (2005)
Qian Wang, Gopal Gupta, Michael Leuschel
Abstract. Provably correct compilation is an important aspect in development of high assurance software systems. In this paper we explore approaches to provably correct code generation based on...
Forward Slicing by Conjunctive Partial Deduction and Argument Filtering (2005)
Michael Leuschel, Germán Vidal
Abstract. Program slicing is a well-known methodology that aims at identifying the program statements that (potentially) affect the values computed at some point of interest. Within imperative...
Stéphane Lo Presti, Michael Butler, Michael Leuschel, Chris Booth
Abstract. We present an analysis Trust Analysis Methodology for finding trust issues within pervasive computing systems. It is based on a systematic analysis of scenarios that describe the typical...
ProTest: An Automatic Test Environment for B Specifications (2004)
Satpathy, Manoranjan, Leuschel, Michael, Butler, Michael
We present ProTest, an automatic test environment for B specifications. B is a model-oriented notation where systems are specified in terms of abstract states and operations on abstract states....
ProTest: An Automatic Test Environment for B Specifications (2004)
Satpathy, Manoranjan, Leuschel, Michael, Butler, Michael
We present ProTest, an automatic test environment for B specifications. B is a model-oriented notation where systems are specified in terms of abstract states and operations on abstract states....
ProTest: An Automatic Test Environment for B Specifications (2004)
Satpathy, Manoranjan, Leuschel, Michael, Butler, Michael
We present ProTest, an automatic test environment for B specifications. B is a model-oriented notation where systems are specified in terms of abstract states and operations on abstract states....
Specializing Interpreters using Offline Partial Deduction (2004)
Leuschel, Michael, Craig, Stephen, Bruynooghe, Maurice, Vanhoof, Wim
We present the latest version of the Logen partial evaluation system for logic programs. In particular we present new binding-types, and show how they can be used to effectively specialise a wide...
Visualising Larger State Spaces in ProB (2004)
ProB is an animator and model checker for the B method. It also allows to visualise the state space of a B machine in graphical way. This is often very useful and allows users to quickly spot whether...
Specializing Interpreters using Offline Partial Deduction (2004)
Leuschel, Michael, Craig, Stephen, Bruynooghe, Maurice, Vanhoof, Wim
We present the latest version of the Logen partial evaluation system for logic programs. In particular we present new binding-types, and show how they can be used to effectively specialise a wide...
Visualising Larger State Spaces in ProB (2004)
ProB is an animator and model checker for the B method. It also allows to visualise the state space of a B machine in graphical way. This is often very useful and allows users to quickly spot whether...
Specializing Interpreters using Offline Partial Deduction (2004)
Leuschel, Michael, Craig, Stephen, Bruynooghe, Maurice, Vanhoof, Wim
We present the latest version of the Logen partial evaluation system for logic programs. In particular we present new binding-types, and show how they can be used to effectively specialise a wide...
Visualising Larger State Spaces in ProB (2004)
ProB is an animator and model checker for the B method. It also allows to visualise the state space of a B machine in graphical way. This is often very useful and allows users to quickly spot whether...
Formal Modelling and Verification of Trust in a Pervasive Application (2004)
Lo Presti, Stephane, Butler, Michael, Leuschel, Michael, Snook, Colin, Turner, Phillip
This report is deliverable WP4-01 of the project “Trusted Software Agents and Services for Pervasive Information Environments.” The deliverable reports on the activities of formal modelling and...
Formal Modelling and Verification of Trust in a Pervasive Application (2004)
Lo Presti, Stephane, Butler, Michael, Leuschel, Michael, Snook, Colin, Turner, Phillip
This report is deliverable WP4-01 of the project “Trusted Software Agents and Services for Pervasive Information Environments.” The deliverable reports on the activities of formal modelling and...
Formal Modelling and Verification of Trust in a Pervasive Application (2004)
Lo Presti, Stephane, Butler, Michael, Leuschel, Michael, Snook, Colin, Turner, Phillip
This report is deliverable WP4-01 of the project “Trusted Software Agents and Services for Pervasive Information Environments.” The deliverable reports on the activities of formal modelling and...
Recently the relationship between abstract interpretation and program specialization has received a lot of scrutiny, and the need has been identified to extend program specialization techniques so to...
Recently the relationship between abstract interpretation and program specialization has received a lot of scrutiny, and the need has been identified to extend program specialization techniques so to...
Recently the relationship between abstract interpretation and program specialization has received a lot of scrutiny, and the need has been identified to extend program specialization techniques so to...
Offline Specialisation in Prolog Using a Hand-Written Compiler Generator (2004)
Leuschel, Michael, Jørgensen, Jesper, Vanhoof, Wim, Bruynooghe, Maurice
The so called "cogen" approach'' to program specialisation, writing a compiler generator instead of a specialiser, has been used with considerable success in partial evaluation of both functional and...
The Use of Formal Methods in the Analysis of Trust (Position Paper) (2004)
Butler, Michael, Leuschel, Michael, Lo Presti, Stephane, Turner, Phillip
Security and trust are two properties of modern computing systems that are thefocus of much recent interest. They play an increasingly significant role in the requirements for modern computing...
ProB: Un outil de modélisation formelle (Invited Talk) (2004)
The development of formal models is often a key step when developing safety or mission critical software. In this setting it is vital to formally check and validate these formal models before...
Lix: An Effective Self-applicable Partial Evaluator for Prolog (2004)
Craig, Stephen-John, Leuschel, Michael
This paper presents a self-applicable partial evaluator for a considerable subset of full Prolog. The partial evaluator is shown to achieve non-trivial specialisation and be effectively self-applied....
Efficient and Flexible Access Control via Logic Program Specialisation (2004)
Barker, Steve, Leuschel, Michael, Varea, Mauricio
We describe the use of a flexible meta-interpreter for performing access control checks on deductive databases. The meta-program is implemented in Prolog and takes as input a database and an access...
Fully Automatic Binding Time Analysis for Prolog (2004)
Craig, Stephen-John, Gallagher, John, Leuschel, Michael, Henriksen, Kim S.
Offline partial evaluation techniques rely on an annotated version of the source program to control the specialisation process. These annotations guide the specialisation and have to ensure...
Offline Specialisation in Prolog Using a Hand-Written Compiler Generator (2004)
Leuschel, Michael, Jørgensen, Jesper, Vanhoof, Wim, Bruynooghe, Maurice
The so called "cogen" approach'' to program specialisation, writing a compiler generator instead of a specialiser, has been used with considerable success in partial evaluation of both functional and...
The Use of Formal Methods in the Analysis of Trust (Position Paper) (2004)
Butler, Michael, Leuschel, Michael, Lo Presti, Stephane, Turner, Phillip
Security and trust are two properties of modern computing systems that are thefocus of much recent interest. They play an increasingly significant role in the requirements for modern computing...
ProB: Un outil de modélisation formelle (Invited Talk) (2004)
The development of formal models is often a key step when developing safety or mission critical software. In this setting it is vital to formally check and validate these formal models before...
Lix: An Effective Self-applicable Partial Evaluator for Prolog (2004)
Craig, Stephen-John, Leuschel, Michael
This paper presents a self-applicable partial evaluator for a considerable subset of full Prolog. The partial evaluator is shown to achieve non-trivial specialisation and be effectively self-applied....
Efficient and Flexible Access Control via Logic Program Specialisation (2004)
Barker, Steve, Leuschel, Michael, Varea, Mauricio
We describe the use of a flexible meta-interpreter for performing access control checks on deductive databases. The meta-program is implemented in Prolog and takes as input a database and an access...
Fully Automatic Binding Time Analysis for Prolog (2004)
Craig, Stephen-John, Gallagher, John, Leuschel, Michael, Henriksen, Kim S.
Offline partial evaluation techniques rely on an annotated version of the source program to control the specialisation process. These annotations guide the specialisation and have to ensure...
Offline Specialisation in Prolog Using a Hand-Written Compiler Generator (2004)
Leuschel, Michael, Jørgensen, Jesper, Vanhoof, Wim, Bruynooghe, Maurice
The so called "cogen" approach'' to program specialisation, writing a compiler generator instead of a specialiser, has been used with considerable success in partial evaluation of both functional and...
The Use of Formal Methods in the Analysis of Trust (Position Paper) (2004)
Butler, Michael, Leuschel, Michael, Lo Presti, Stephane, Turner, Phillip
Security and trust are two properties of modern computing systems that are thefocus of much recent interest. They play an increasingly significant role in the requirements for modern computing...
ProB: Un outil de modélisation formelle (Invited Talk) (2004)
The development of formal models is often a key step when developing safety or mission critical software. In this setting it is vital to formally check and validate these formal models before...
Lix: An Effective Self-applicable Partial Evaluator for Prolog (2004)
Craig, Stephen-John, Leuschel, Michael
This paper presents a self-applicable partial evaluator for a considerable subset of full Prolog. The partial evaluator is shown to achieve non-trivial specialisation and be effectively self-applied....
Efficient and Flexible Access Control via Logic Program Specialisation (2004)
Barker, Steve, Leuschel, Michael, Varea, Mauricio
We describe the use of a flexible meta-interpreter for performing access control checks on deductive databases. The meta-program is implemented in Prolog and takes as input a database and an access...
Fully Automatic Binding Time Analysis for Prolog (2004)
Craig, Stephen-John, Gallagher, John, Leuschel, Michael, Henriksen, Kim S.
Offline partial evaluation techniques rely on an annotated version of the source program to control the specialisation process. These annotations guide the specialisation and have to ensure...
Fully automatic binding-time analysis for Prolog (2004)
Stephen-john Craig, John P. Gallagher, Michael Leuschel, Kim S
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...
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...
Model checking object Petri nets in Prolog (2004)
Berndt Farwer, Berndt Farwer, Michael Leuschel, Michael Leuschel
Abstract Object Petri nets (OPNs) provide a natural and modular method for the modelling of many real-world systems. We give a structure-preserving translation of OPNs to Prolog, avoiding the need...
Specialising interpreters using offline partial deduction (2004)
Michael Leuschel, Stephen J. Craig, Maurice Bruynooghe, Wim Vanhoof
Abstract. We present the latest version of the logen partial evaluation system for logic programs. In particular we present new binding-types, and show how they can be used to effectively specialise...
Offline specialisation in Prolog using a hand-written compiler generator (2004)
Michael Leuschel, Jesper Jørgensen
The so called âcogen approachâ to program specialisation, writing a compiler generator instead of a specialiser, has been used with considerable success in partial evaluation of both...
Specialising interpreters using offline partial deduction (2004)
Michael Leuschel, Stephen J. Craig, Maurice Bruynooghe, Wim Vanhoof
Abstract. We present the latest version of the logen partial evaluation system for logic programs. In particular we present new binding-types, and show how they can be used to effectively specialise...
Zhenjiang Hu, Shin-cheng Mu, Nevin Heintze, Julia Lawall, Michael Leuschel, Peter Sestoft
Abstract. This paper presents an application of bidirectional transformations to design and implementation of a novel editor supporting interactive refinement in the development of structured...
Zhenjiang Hu, Shin-cheng Mu, Nevin Heintze, Julia Lawall, Michael Leuschel, Peter Sestoft
Abstract. This paper presents an application of bidirectional transformation to the design and implementation of a novel editor supporting interactive refinement in the development of structured...
Lix: An effective self-applicable partial evaluator for Prolog (2004)
Stephen-john Craig, Michael Leuschel
Abstract. This paper presents a self-applicable partial evaluator for a considerable subset of full Prolog. The partial evaluator is shown to achieve non-trivial specialisation and be effectively...
Binding-time analysis for Mercury (2004)
In this work, we develop a binding-time analysis for the logic programming language Mercury. We introduce a precise domain of binding-times, based on the type information available in Mercury...
Model Checking of Object Petri Nets in Prolog (2003)
Farwer, Berndt, Leuschel, Michael
Object Petri nets (OPNs) provide a natural and modular method for the modelling of many real-world systems. We give a structure-preserving translation of OPNs to Prolog, avoiding the need for an...
Specializing Interpreters using Offline Partial Deduction (2003)
Leuschel, Michael, Craig, Stephen, Bruynooghe, Maurice, Vanhoof, Wim
We present the latest version of the {\sc logen} partial evaluation system for logic programs. In particular we present new binding-types, and show how they can be used to effectively specialise a...
Model Checking of Object Petri Nets in Prolog (2003)
Farwer, Berndt, Leuschel, Michael
Object Petri nets (OPNs) provide a natural and modular method for the modelling of many real-world systems. We give a structure-preserving translation of OPNs to Prolog, avoiding the need for an...
Specializing Interpreters using Offline Partial Deduction (2003)
Leuschel, Michael, Craig, Stephen, Bruynooghe, Maurice, Vanhoof, Wim
We present the latest version of the {\sc logen} partial evaluation system for logic programs. In particular we present new binding-types, and show how they can be used to effectively specialise a...
Model Checking of Object Petri Nets in Prolog (2003)
Farwer, Berndt, Leuschel, Michael
Object Petri nets (OPNs) provide a natural and modular method for the modelling of many real-world systems. We give a structure-preserving translation of OPNs to Prolog, avoiding the need for an...
Specializing Interpreters using Offline Partial Deduction (2003)
Leuschel, Michael, Craig, Stephen, Bruynooghe, Maurice, Vanhoof, Wim
We present the latest version of the {\sc logen} partial evaluation system for logic programs. In particular we present new binding-types, and show how they can be used to effectively specialise a...
Proceedings of the 3rd Workshop on Automated Verification of Critical Systems (AVoCS'03) (2003)
Leuschel, Michael, Gruner, Stefan, Lo Presti, Stephane
The aim of this workshop is to foster a research community in verification in and beyond the United Kingdom of Great Britain through encouraging communication among researchers. Specific objectives...
Proceedings of the 3rd Workshop on Automated Verification of Critical Systems (AVoCS'03) (2003)
Leuschel, Michael, Gruner, Stefan, Lo Presti, Stephane
The aim of this workshop is to foster a research community in verification in and beyond the United Kingdom of Great Britain through encouraging communication among researchers. Specific objectives...
Proceedings of the 3rd Workshop on Automated Verification of Critical Systems (AVoCS'03) (2003)
Leuschel, Michael, Gruner, Stefan, Lo Presti, Stephane
The aim of this workshop is to foster a research community in verification in and beyond the United Kingdom of Great Britain through encouraging communication among researchers. Specific objectives...
Towards a Trust Analysis Framework for Pervasive Computing Scenarios (2003)
Butler, Michael, Leuschel, Michael, Lo Presti, Stephane, Allsopp, David, Beautement, Patrick, Booth, Chris, ...
We present a scheme for highlighting the trust issues of merit within pervasive computing, based on an analysis of scenarios from the healthcare domain. The first scenario helps us define an analysis...
Using the Extensible Model Checker XTL to Verify StAC Business Specifications (2003)
Augusto, Juan Carlos, Leuschel, Michael, Butler, Michael, Ferreira, Carla
The Benefits of Rapid Modelling for E-Business System Development (2003)
Augusto, Juan C., Ferreira, Carla, Gravell, Andy M., Leuschel, Michael, NG, Karen M.Y.
Improving Compositional Verification of State-based Models by Reducing Modular Unbalance (2003)
Varea, Mauricio, Leuschel, Michael, Al-Hashimi, Bashir
Compositional Verification is a viable way to tackle the state explosion problem. However, the decomposition of a system into smaller parts is not a trivial problem, and dividing the specification...
Partial Evaluation of MATLAB (2003)
Elphick, Daniel, Leuschel, Michael, Cox, Simon
We describe the problems associated with the creation of high performance code for mathematical computations. We discuss the advantages and disadvantages of using a high level language like MATLAB...
A Compiler Generator for Constraint Logic Programs (2003)
Craig, Stephen, Leuschel, Michael
The Cogen approach to program specialisation, writing a compiler generator instead of a specialiser, has been used with considerable success. This paper demonstrates that the Cogen approach is also...
ProB: A Model Checker for B (2003)
Leuschel, Michael, Butler, Michael
We present ProB, an animation and model checking tool for the B method. ProB's animation facilities allow users to gain confidence in their specifications, and unlike the animator provided by the...
Lehmann, Helko, Leuschel, Michael
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...
Lehmann, Helko, Leuschel, Michael
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...
Towards a Trust Analysis Framework for Pervasive Computing Scenarios (2003)
Butler, Michael, Leuschel, Michael, Lo Presti, Stephane, Allsopp, David, Beautement, Patrick, Booth, Chris, ...
We present a scheme for highlighting the trust issues of merit within pervasive computing, based on an analysis of scenarios from the healthcare domain. The first scenario helps us define an analysis...
Using the Extensible Model Checker XTL to Verify StAC Business Specifications (2003)
Augusto, Juan Carlos, Leuschel, Michael, Butler, Michael, Ferreira, Carla
The Benefits of Rapid Modelling for E-Business System Development (2003)
Augusto, Juan C., Ferreira, Carla, Gravell, Andy M., Leuschel, Michael, NG, Karen M.Y.
Improving Compositional Verification of State-based Models by Reducing Modular Unbalance (2003)
Varea, Mauricio, Leuschel, Michael, Al-Hashimi, Bashir
Compositional Verification is a viable way to tackle the state explosion problem. However, the decomposition of a system into smaller parts is not a trivial problem, and dividing the specification...
Partial Evaluation of MATLAB (2003)
Elphick, Daniel, Leuschel, Michael, Cox, Simon
We describe the problems associated with the creation of high performance code for mathematical computations. We discuss the advantages and disadvantages of using a high level language like MATLAB...
A Compiler Generator for Constraint Logic Programs (2003)
Craig, Stephen, Leuschel, Michael
The Cogen approach to program specialisation, writing a compiler generator instead of a specialiser, has been used with considerable success. This paper demonstrates that the Cogen approach is also...
ProB: A Model Checker for B (2003)
Leuschel, Michael, Butler, Michael
We present ProB, an animation and model checking tool for the B method. ProB's animation facilities allow users to gain confidence in their specifications, and unlike the animator provided by the...
Lehmann, Helko, Leuschel, Michael
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...
Lehmann, Helko, Leuschel, Michael
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...
Towards a Trust Analysis Framework for Pervasive Computing Scenarios (2003)
Butler, Michael, Leuschel, Michael, Lo Presti, Stephane, Allsopp, David, Beautement, Patrick, Booth, Chris, ...
We present a scheme for highlighting the trust issues of merit within pervasive computing, based on an analysis of scenarios from the healthcare domain. The first scenario helps us define an analysis...
Using the Extensible Model Checker XTL to Verify StAC Business Specifications (2003)
Augusto, Juan Carlos, Leuschel, Michael, Butler, Michael, Ferreira, Carla
The Benefits of Rapid Modelling for E-Business System Development (2003)
Augusto, Juan C., Ferreira, Carla, Gravell, Andy M., Leuschel, Michael, NG, Karen M.Y.
Improving Compositional Verification of State-based Models by Reducing Modular Unbalance (2003)
Varea, Mauricio, Leuschel, Michael, Al-Hashimi, Bashir
Compositional Verification is a viable way to tackle the state explosion problem. However, the decomposition of a system into smaller parts is not a trivial problem, and dividing the specification...
Partial Evaluation of MATLAB (2003)
Elphick, Daniel, Leuschel, Michael, Cox, Simon
We describe the problems associated with the creation of high performance code for mathematical computations. We discuss the advantages and disadvantages of using a high level language like MATLAB...
A Compiler Generator for Constraint Logic Programs (2003)
Craig, Stephen, Leuschel, Michael
The Cogen approach to program specialisation, writing a compiler generator instead of a specialiser, has been used with considerable success. This paper demonstrates that the Cogen approach is also...
ProB: A Model Checker for B (2003)
Leuschel, Michael, Butler, Michael
We present ProB, an animation and model checking tool for the B method. ProB's animation facilities allow users to gain confidence in their specifications, and unlike the animator provided by the...
Lehmann, Helko, Leuschel, Michael
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...
Lehmann, Helko, Leuschel, Michael
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...
ProB: A model checker for B (2003)
Michael Leuschel, Michael Butler
Abstract. We present ProB, an animation and model checking tool for the B method. ProB’s animation facilities allow users to gain confidence in their specifications, and unlike the animator...
Partial evaluation of MATLAB (2003)
Daniel Elphick, Michael Leuschel, Simon Cox
Abstract. We describe the problems associated with the creation of high performance code for mathematical computations. We discuss the advantages and disadvantages of using a high level language like...
Towards a Trust Analysis Framework for Pervasive Computing Scenarios (2003)
Michael Butler, Michael Leuschel, Stéphane Lo Presti, David Allsopp
We present a scheme for highlighting the trust issues of merit within pervasive computing, based on an analysis of scenarios from the healthcare domain. The first scenario helps us define an analysis...
Using the extensible model checker XTL to verify StAC Business Specifications (2003)
Juan C. Augusto, Michael Leuschel, Michael Butler, Carla Ferreira
StAC is a business specification language that has been developed as part of a partnership program between IBM UK Labs. and the University of Southampton. It is highly desirable for Business...
Using the extensible model checker XTL to verify StAC business specifications (2003)
Juan C. Augusto, Michael Leuschel, Michael Butler, Carla Ferreira
Abstract. StAC is a business specification language that has been developed as part of a partnership program between IBM UK Labs. and the University of Southampton. It is highly desirable for...
Partial evaluation of MATLAB (2003)
Daniel Elphick, Michael Leuschel, Simon Cox
Abstract. We describe the problems associated with the creation of high performance code for mathematical computations. We discuss the advantages and disadvantages of using a high level language like...
Generating inductive verification proofs for Isabelle using the partial evaluator Ecce (2002)
Lehmann, Helko, Leuschel, Michael
Ecce is a partial deduction system which can be used to automatically generate abstractions for the model checking of many infinite state systems. We show that to verify the abstractions generated by...
Generating inductive verification proofs for Isabelle using the partial evaluator Ecce (2002)
Lehmann, Helko, Leuschel, Michael
Ecce is a partial deduction system which can be used to automatically generate abstractions for the model checking of many infinite state systems. We show that to verify the abstractions generated by...
Generating inductive verification proofs for Isabelle using the partial evaluator Ecce (2002)
Lehmann, Helko, Leuschel, Michael
Ecce is a partial deduction system which can be used to automatically generate abstractions for the model checking of many infinite state systems. We show that to verify the abstractions generated by...
Offline Specialisation in Prolog Using a Hand-Written Compiler Generator (2002)
Leuschel, Michael, Joergensen, Jesper, Vanhoof, Wim, Bruynooghe, Maurice
The so called ``cogen approach'' to program specialisation, writing a compiler generator instead of a specialiser, has been used with considerable success in partial evaluation of both functional and...
Logic program specialisation through partial deduction: Control Issues (2002)
Leuschel, Michael, Bruynooghe, Maurice
Program specialisation aims at improving the overall performance of programs by performing source to source transformations. A common approach within functional and logic programming, known...
Logic program specialisation through partial deduction: Control Issues (2002)
Leuschel, Michael, Bruynooghe, Maurice
Program specialisation aims at improving the overall performance of programs by performing source to source transformations. A common approach within functional and logic programming, known...
Logic program specialisation through partial deduction: Control Issues (2002)
Leuschel, Michael, Bruynooghe, Maurice
Program specialisation aims at improving the overall performance of programs by performing source to source transformations. A common approach within functional and logic programming, known...
Logic program specialisation through partial deduction: Control issues (2002)
Leuschel, Michael, Bruynooghe, Maurice
Program specialisation aims at improving the overall performance of programs by performing source to source transformations. A common approach within functional and logic programming, known...
Leuschel, Michael, Gruner, Stefan
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...
Leuschel, Michael, Gruner, Stefan
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...
Homeomorphic Embedding for Online Termination of Symbolic Methods (2002)
Well-quasi orders in general, and homeomorphic embedding in particular, have gained popularity to ensure the termination of techniques for program analysis, specialisation, transformation, and...
Leuschel, Michael, Massart, Thierry
In earlier work it has been shown that finite state CTL model checking of reactive systems can be achieved by a relatively simple interpreter written in tabled logic programming. This approach is...
Leuschel, Michael, Gruner, Stefan
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...
Leuschel, Michael, Gruner, Stefan
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...
Homeomorphic Embedding for Online Termination of Symbolic Methods (2002)
Well-quasi orders in general, and homeomorphic embedding in particular, have gained popularity to ensure the termination of techniques for program analysis, specialisation, transformation, and...
Leuschel, Michael, Massart, Thierry
In earlier work it has been shown that finite state CTL model checking of reactive systems can be achieved by a relatively simple interpreter written in tabled logic programming. This approach is...
Leuschel, Michael, Gruner, Stefan
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...
Leuschel, Michael, Gruner, Stefan
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...
Homeomorphic Embedding for Online Termination of Symbolic Methods (2002)
Well-quasi orders in general, and homeomorphic embedding in particular, have gained popularity to ensure the termination of techniques for program analysis, specialisation, transformation, and...
Leuschel, Michael, Massart, Thierry
In earlier work it has been shown that finite state CTL model checking of reactive systems can be achieved by a relatively simple interpreter written in tabled logic programming. This approach is...
Generating inductive verification proofs for Isabelle using the partial evaluator Ecce (2002)
Helko Lehmann, Michael Leuschel, Helko Lehmann, Michael Leuschel
Generating inductive verification proofs for Isabelle using
Michael Leuschel, Thierry Massart
Abstract. In earlier work it has been shown that finite state CTL model checking of reactive systems can be achieved by a relatively simple interpreter written in tabled logic programming. This...
Design and Implementation of the High-Level Specification Language CSP(LP) (2001)
We describe practical experiences of using a logic programming based approach to model and reason about concurrent systems. We argue that logic programming is a good foundation for developing,...
Design and Implementation of the High-Level Specification Language CSP(LP) (2001)
We describe practical experiences of using a logic programming based approach to model and reason about concurrent systems. We argue that logic programming is a good foundation for developing,...
Design and Implementation of the High-Level Specification Language CSP(LP) (2001)
We describe practical experiences of using a logic programming based approach to model and reason about concurrent systems. We argue that logic programming is a good foundation for developing,...
Design and Implementation of the High-Level Specification Language CSP(LP) (2001)
We describe practical experiences of using a logic programming based approach to model and reason about concurrent systems. We argue that logic programming is a good foundation for developing,...
Design and Implementation of the High-Level Specification Language CSP(LP) (2001)
We describe practical experiences of using a logic programming based approach to model and reason about concurrent systems. We argue that logic programming is a good foundation for developing,...
Design and Implementation of the High-Level Specification Language CSP(LP) (2001)
We describe practical experiences of using a logic programming based approach to model and reason about concurrent systems. We argue that logic programming is a good foundation for developing,...
Proceedings of the ACM Sigplan Workshop on Verification and Computational Logic VCL'2001 (2001)
Leuschel, Michael, Podelski, Andreas, Ramakrishnan, C.R., Ultes-Nitsche, Ulrich
Animation and Model Checking of CSP and B using Prolog Technology (2001)
Leuschel, Michael, Adhianto, Laksono, Butler, Michael, Ferreira, Carla, Mikhailov, Leonid
We describe practical experiences of using a logic programming based approach to model and reason about critical systems. We argue that logic programming with co-routining, constraints, and tabling...
Proceedings of the ACM Sigplan Workshop on Verification and Computational Logic VCL'2001 (2001)
Leuschel, Michael, Podelski, Andreas, Ramakrishnan, C.R., Ultes-Nitsche, Ulrich
Animation and Model Checking of CSP and B using Prolog Technology (2001)
Leuschel, Michael, Adhianto, Laksono, Butler, Michael, Ferreira, Carla, Mikhailov, Leonid
We describe practical experiences of using a logic programming based approach to model and reason about critical systems. We argue that logic programming with co-routining, constraints, and tabling...
Proceedings of the ACM Sigplan Workshop on Verification and Computational Logic VCL'2001 (2001)
Leuschel, Michael, Podelski, Andreas, Ramakrishnan, C.R., Ultes-Nitsche, Ulrich
Animation and Model Checking of CSP and B using Prolog Technology (2001)
Leuschel, Michael, Adhianto, Laksono, Butler, Michael, Ferreira, Carla, Mikhailov, Leonid
We describe practical experiences of using a logic programming based approach to model and reason about critical systems. We argue that logic programming with co-routining, constraints, and tabling...
Strategy for Improving Memory Locality Reuse and Exploiting Hidden Parallelism (2001)
Adhianto, Laksono, Leuschel, Michael
In recent years, methods for analyzing and parallelizing sequential code using data analysis and loop transformations have been developed. These techniques have proved remarkably successful, and have...
Strategy for Improving Memory Locality Reuse and Exploiting Hidden Parallelism (2001)
Adhianto, Laksono, Leuschel, Michael
In recent years, methods for analyzing and parallelizing sequential code using data analysis and loop transformations have been developed. These techniques have proved remarkably successful, and have...
Strategy for Improving Memory Locality Reuse and Exploiting Hidden Parallelism (2001)
Adhianto, Laksono, Leuschel, Michael
In recent years, methods for analyzing and parallelizing sequential code using data analysis and loop transformations have been developed. These techniques have proved remarkably successful, and have...
Temporal Logic Model Checking of CSP: Tools and Techniques (2001)
Leuschel, Michael, Wolton, Ivan, Massart, Thierry, Adhianto, Laksono
We study the possibility of doing LTL model checking on CSP specifications in the context of refinement. We present a technique to perform LTL model checking of CSP processes using refinement...
Temporal Logic Model Checking of CSP: Tools and Techniques (2001)
Leuschel, Michael, Wolton, Ivan, Massart, Thierry, Adhianto, Laksono
We study the possibility of doing LTL model checking on CSP specifications in the context of refinement. We present a technique to perform LTL model checking of CSP processes using refinement...
Temporal Logic Model Checking of CSP: Tools and Techniques (2001)
Leuschel, Michael, Wolton, Ivan, Massart, Thierry, Adhianto, Laksono
We study the possibility of doing LTL model checking on CSP specifications in the context of refinement. We present a technique to perform LTL model checking of CSP processes using refinement...
How to make FDR Spin: LTL model checking of CSP using Refinement (2001)
Leuschel, Michael, Massart, Thierry, Currie, Andrew
We study the possibility of doing LTL model checking on CSP specifications in the context of refinement. We present evidence that the refinement-based approach to verification does not seem to be...
How to make FDR Spin: LTL model checking of CSP using Refinement (2001)
Leuschel, Michael, Massart, Thierry, Currie, Andrew
We study the possibility of doing LTL model checking on CSP specifications in the context of refinement. We present evidence that the refinement-based approach to verification does not seem to be...
How to make FDR Spin: LTL model checking of CSP using Refinement (2001)
Leuschel, Michael, Massart, Thierry, Currie, Andrew
We study the possibility of doing LTL model checking on CSP specifications in the context of refinement. We present evidence that the refinement-based approach to verification does not seem to be...
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...
Animation and model checking of csp and b using prolog technology (2001)
Michael Leuschel, Laksono Adhianto, Michael Butler, Carla Ferreira, Leonid Mikhailov
Abstract. We describe practical experiences of using a logic programming based approach to model and reason about critical systems. We argue that logic programming with co-routining, constraints, and...
Animation and model checking of csp and b using prolog technology (2001)
Michael Leuschel, Laksono Adhianto, Michael Butler, Carla Ferreira, Leonid Mikhailov
Abstract. We describe practical experiences of using a logic programming based approach to model and reason about critical systems. We argue that logic programming with co-routining, constraints, and...
Control Issues in Partial Deduction: The Ever Ending Story (2000)
Leuschel, Michael, Bruynooghe, Maurice
Partial deduction is a source-to-source technique for specialising logic programs. This is (mostly) done by a well-automated application of parts of the Burstall and Darlington unfold/fold...
Control Issues in Partial Deduction: The Ever Ending Story (2000)
Leuschel, Michael, Bruynooghe, Maurice
Partial deduction is a source-to-source technique for specialising logic programs. This is (mostly) done by a well-automated application of parts of the Burstall and Darlington unfold/fold...
Control Issues in Partial Deduction: The Ever Ending Story (2000)
Leuschel, Michael, Bruynooghe, Maurice
Partial deduction is a source-to-source technique for specialising logic programs. This is (mostly) done by a well-automated application of parts of the Burstall and Darlington unfold/fold...
Solving Coverability Problems of Petri Nets by Partial Deduction (2000)
Leuschel, Michael, Lehmann, Helko
In recent work it has been shown that infinite state model checking can be performed by a combination of partial deduction of logic programs and abstract interpretation. This paper focuses on one...
Solving Coverability Problems of Petri Nets by Partial Deduction (2000)
Leuschel, Michael, Lehmann, Helko
In recent work it has been shown that infinite state model checking can be performed by a combination of partial deduction of logic programs and abstract interpretation. This paper focuses on one...
Solving Coverability Problems of Petri Nets by Partial Deduction (2000)
Leuschel, Michael, Lehmann, Helko
In recent work it has been shown that infinite state model checking can be performed by a combination of partial deduction of logic programs and abstract interpretation. This paper focuses on one...
Solving Coverability Problems of Petri Nets by Partial Deduction (2000)
Leuschel, Michael, Lehmann, Helko
In recent work it has been shown that infinite state model checking can be performed by a combination of partial deduction of logic programs and abstract interpretation. This paper focuses on one...
Solving Coverability Problems of Petri Nets by Partial Deduction (2000)
Leuschel, Michael, Lehmann, Helko
In recent work it has been shown that infinite state model checking can be performed by a combination of partial deduction of logic programs and abstract interpretation. This paper focuses on one...
Solving Coverability Problems of Petri Nets by Partial Deduction (2000)
Leuschel, Michael, Lehmann, Helko
In recent work it has been shown that infinite state model checking can be performed by a combination of partial deduction of logic programs and abstract interpretation. This paper focuses on one...
Leuschel, Michael, Lehmann, Helko
In recent work it has been shown that infinite state model checking can be performed by a combination of partial deduction of logic programs and abstract interpretation. It has also been shown that...
LTL Model Checking of CSP by Refinement: How to Make FDR Spin (2000)
Currie, Andrew, Leuschel, Michael, Massart, Thierry
We show how to (and how not to) perform LTL model checking of CSP processes using refinement checking in general and the FDR tool in particular. We show how one can handle (potentially) deadlocking...
Proceedings of the Workshop on Verification and Computational Logic VCL'2000 (2000)
Leuschel, Michael, Podelski, Andreas, Ramakrishnan, C.R., Ultes-Nitsche, Ulrich
The aim of this workshop is to bring together researchers working on the interplay between verification techniques (e.g., model checking, reduction, and abstraction) and logic programming techniques...
Leuschel, Michael, Lehmann, Helko
In recent work it has been shown that infinite state model checking can be performed by a combination of partial deduction of logic programs and abstract interpretation. It has also been shown that...
LTL Model Checking of CSP by Refinement: How to Make FDR Spin (2000)
Currie, Andrew, Leuschel, Michael, Massart, Thierry
We show how to (and how not to) perform LTL model checking of CSP processes using refinement checking in general and the FDR tool in particular. We show how one can handle (potentially) deadlocking...
Proceedings of the Workshop on Verification and Computational Logic VCL'2000 (2000)
Leuschel, Michael, Podelski, Andreas, Ramakrishnan, C.R., Ultes-Nitsche, Ulrich
The aim of this workshop is to bring together researchers working on the interplay between verification techniques (e.g., model checking, reduction, and abstraction) and logic programming techniques...
Leuschel, Michael, Lehmann, Helko
In recent work it has been shown that infinite state model checking can be performed by a combination of partial deduction of logic programs and abstract interpretation. It has also been shown that...
LTL Model Checking of CSP by Refinement: How to Make FDR Spin (2000)
Currie, Andrew, Leuschel, Michael, Massart, Thierry
We show how to (and how not to) perform LTL model checking of CSP processes using refinement checking in general and the FDR tool in particular. We show how one can handle (potentially) deadlocking...
Proceedings of the Workshop on Verification and Computational Logic VCL'2000 (2000)
Leuschel, Michael, Podelski, Andreas, Ramakrishnan, C.R., Ultes-Nitsche, Ulrich
The aim of this workshop is to bring together researchers working on the interplay between verification techniques (e.g., model checking, reduction, and abstraction) and logic programming techniques...
A Polyvariant Binding-Time Analysis for Off-line Partial Deduction (2000)
Bruynooghe, Maurice, Leuschel, Michael, Sagonas, Konstantinos
We study the notion of binding-time analysis for logic programs. We formalise the unfolding aspect of an on-line partial deduction system as a Prolog program. Using abstract interpretation, we...
Michael Leuschel, Helko Lehmann
Abstract. In recent work it has been shown that infinite state model checking can be performed by a combination of partial deduction of logic programs and abstract interpretation. It has also been...
Solving planning problems by partial deduction (2000)
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...
Solving coverability problems of Petri nets by partial deduction (2000)
Michael Leuschel, Helko Lehmann
In recent work it has been shown that innite state model checking can be performed by a combination of partial deduction of logic programs and abstract interpretation. This paper focuses on a...
Extended Abstract, Robert Glück, Michael Leuschel
We present an approach to software verification by program inversion, exploiting recent progress in the field of automatic program transformation, partial deduction and abstract interpretation....
Completeness of Partial Deduction for Coverability Problems of Petri Nets (2000)
Michael Leuschel, Helko Lehmann
In recent work it has been shown that infinite state model checking can be performed by a combination of partial deduction of logic programs and abstract interpretation. This paper characterises some...
ProTest: An Automatic Test Environment for B Specifications (2000)
Manoranjan Satpathy Michael, Michael Leuschel, Michael Butler
We present ProTest, an automatic test environment for B specifications. B is a model-oriented notation where systems are specified in terms of abstract states and operations on abstract states....
Efficient Specialisation in Prolog Using a Hand-Written Compiler Generator (1999)
Michael Leuschel, Jesper Jørgensen, Michael Leuschel
The so called "cogen approach" to program specialisation, writing a compiler generator instead of a specialiser, has been used with considerable success in partial evaluation of both...
Questions and Answers about Ten Formal Methods (1999)
Pieter Hartel, Michael Butler, Andrew Currie, Peter Henderson, Michael Leuschel, Andrew Martin, ...
An abstract model of a distributed data base application has been studied using process based, state based, and queueing theory based methods. The methods supported by graphical notations and/or...
Sonic Partial Deduction (1999)
Jonathan Martin, Jonathan Martin, Michael Leuschel, Michael Leuschel
. The current state of the art for ensuring finite unfolding of logic programs consists of a number of online techniques where unfolding decisions are made at specialisation time. Introduction of a...
Binding-time analysis for Mercury (1999)
Wim Vanhoof, Maurice Bruynooghe, Michael Leuschel
Abstract. In this work, we develop a binding-time analysis for the logic programming language Mercury. We introduce a precise domain of binding-times, based on the type information available in...
Infinite state model checking by abstract interpretation and program specialisation (1999)
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...
Sonic partial deduction (1998)
Jonathan Martin, Michael Leuschel
The current state of the art for ensuring finite unfolding of logic programs consists of a number of online techniques where unfolding decisions are made at specialisation time. Introduction of a...
Symmetry reduction for B by permutation flooding (1998)
Michael Leuschel, Michael Butler, Corinna Spermann, Edd Turner
Abstract. Symmetry reduction is an established method for limiting the amount of states that have to be checked during exhaustive model checking. The idea is to only verify a single representative of...
Controlling generalization and polyvariance in partial deduction of normal logic programs (1998)
Michael Leuschel, Bern Martens, Danny De Schreye
Given a program and some input data, partial deduction computes a specialized program handling any remaining input more efficiently. However, controlling the process well is a rather difficult...
On the Power of Homeomorphic Embedding for Online Termination (1998)
Michael Leuschel, Michael Leuschel
Abstract. Recently well-quasi orders in general, and homeomorphic embedding in particular, have gained popularity to ensure the termination of program analysis, specialisation and transformation...
Some achievements and prospects in partial deduction (1998)
Michael Leuschel, Bern Martens, Danny De Schreye
In the context of logic programming the full input to a program P consists of a goal G and evaluation corresponds to constructing a complete SLDNF-tree for P [fGg. Partial evaluation in such a...
Termination analysis for tabled logic programming (1998)
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 leftto-right computation rule. To this end, we study the classes...
Schreye. Constrained partial deduction and the preservation of characteristic trees (1998)
Michael Leuschel, Danny De Schreye
Partial deduction strategies for logic programs often use an abstraction operator to guarantee the finiteness of the set of goals for which partial deductions are produced. Finding an abstraction...
A polyvariant binding-time analysis for off-line partial deduction (1998)
Maurice Bruynooghe, Michael Leuschel, Konstantinos Sagonas
Abstract. We study the notion of binding-time analysis for logic programs. We formalise the unfolding aspect of an on-line partial deduction system as a Prolog program. Using abstract interpretation,...
Controlling generalization and polyvariance in partial deduction of normal logic programs (1998)
Michael Leuschel, Bern Martens, Danny De Schreye
Given a program and some input data, partial deduction computes a specialized program handling any remaining input more e#ciently. However, controlling the process well is a rather di#cult problem....
Creating Specialised Integrity Checks Through Partial Evaluation of Meta-Interpreters (1998)
Michael Leuschel, Danny De Schreye
Integrity constraints are useful for the specification of deductive databases, as well as for inductive and abductive logic programs. Verifying integrity constraints upon updates is a major...
Homeomorphic Embedding for Online Termination (1998)
Recently well-quasi orders in general, and homeomorphic embedding in particular, have gained popularity to ensure the termination of program analysis, specialisation and transformation techniques. In...
Program specialisation and abstract interpretation reconciled (1998)
We clarify the relationship between abstract interpretation and program specialisation in the context of logic programming. We present a generic top-down abstract specialisation framework, along with...
On the Power of Homeomorphic Embedding for Online Termination (1998)
Abstract. Well-quasi orders in general, and homeomorphic embedding in particular, have gained popularity to ensure online termination of program analysis, specialisation and transformation...
On the Power of Homeomorphic Embedding for Online Termination (1998)
Abstract. Recently well-quasi orders in general, and homeomorphic embedding in particular, have gained popularity to ensure the termination of program analysis, specialisation and transformation...
A polyvariant binding-time analysis for off-line partial deduction (1998)
Maurice Bruynooghe, Michael Leuschel, Konstantinos Sagonas
Abstract. We study the notion of binding-time analysis for logic programs. We formalise the unfolding aspect of an on-line partial deduction system as a Prolog program. Using abstract interpretation,...
Preserving Termination of Tabled Logic Programs While Unfolding (1997)
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...
Constrained partial deduction (1997)
Michael Leuschel, Danny De Schreye
Partial deduction based upon the Lloyd and Shepherdson framework generates a specialised program given a set of atoms. Each such atom represents all its instances. This can severely limit the...
Partial Deduction System (1997)
We present the fully automatic partial deduction system ecce, which can be used to specialise and optimise logic programs. We describe the underlying principles of ecce and illustrate some of the...
Controlling Generalisation and Polyvariance in Partial Deduction of Normal Logic Programs (1997)
Controlling Generalisation, Michael Leuschel, Michael Leuschel, Bern Martens, Bern Martens, Danny De Schreye, ...
In this paper, we further elaborate global control for partial deduction: For which atoms, among possibly infinitely many, should partial deductions be produced, meanwhile guaranteeing correctness as...
Extending Homeomorphic Embedding in the Context of Logic Programming (1997)
Recently well-quasi orders in general, and homeomorphic embedding in particular, have gained popularity to ensure the termination of program analysis, specialisation and transformation techniques....
Constrained Partial Deduction and the Preservation of Characteristic Trees (1997)
Michael Leuschel, Michael Leuschel, Danny De Schreye, Danny De Schreye
Partial deduction strategies for logic programs often use an abstraction operator to guarantee the finiteness of the set of goals for which partial deductions are produced. Finding an abstraction...
Extending Homeomorphic Embedding in the Context of Logic Programming (1997)
Recently well-quasi orders in general, and homeomorphic embedding in particular, have gained popularity to ensure the termination of program analysis, specialisation and transformation techniques....
Constrained Partial Deduction (1997)
Michael Leuschel, Danny De Schreye
Partial deduction based upon the Lloyd and Shepherdson framework generates a specialised program given a set of atoms. Each such atom represents all its instances. This can severely limit the...
Extending Homeomorphic Embedding in the Context of Logic Programming (1997)
Michael Leuschel, Michael Leuschel
Recently well-quasi orders in general, and homeomorphic embedding in particular, have gained popularity to ensure the termination of program analysis, specialisation and transformation techniques....
Advanced Techniques for Logic Program Specialisation (1997)
Program specialisation, also called partial evaluation or partial deduction, is an automatic technique for program optimisation. The central idea is to specialise a given source program for a...
Preserving Termination of Tabled Logic Programs While Unfolding (1997)
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...
The ecce Partial Deduction System (1997)
We present the fully automatic partial deduction system ecce, which can be used to specialise and optimise logic programs. We describe the underlying principles of ecce and illustrate some of the...
Conjunctive Partial Deduction in Practice (1996)
Jesper Jørgensen, Michael Leuschel, Bern Martens
. 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...
Redundant Argument Filtering of Logic Programs (1996)
Michael Leuschel, Morten Heine Sørensen
This paper is concerned with the problem of removing, from a given logic program, redundant arguments. These are arguments which can be removed without affecting correctness. Most program...
Logic Program Specialisation: How To Be More Specific (1996)
Michael Leuschel, Danny De Schreye
Standard partial deduction suffers from several drawbacks when compared to topdown abstract interpretation schemes. Conjunctive partial deduction, an extension of standard partial deduction, remedies...
Redundant Argument Filtering of Logic Programs (1996)
Michael Leuschel, Morten Heine S��rensen
. 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...
Efficiently generating efficient generating extensions in Prolog (1996)
Jesper Jørgensen, Michael Leuschel
Abstract. The so called “cogen approach ” to program specialisation, writing a compiler generator instead of a specialiser, has been used with considerable success in partial evaluation of both...
Schreye. Logic program specialisation: How to be more specific (1996)
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...
Conjunctive partial deduction in practice (1996)
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...
Partial Deduction of the Ground Representation and its Application to Integrity Checking (1995)
Michael Leuschel, Bern Martens
Integrity constraints are very useful in many contexts, such as, for example, deductive databases, abductive and inductive logic programming. However, fully testing the integrity constraints after...
Michael Leuschel, Bern Martens
Integrity constraints are very useful in many contexts, such as, for example, deductive databases, abductive and inductive logic programming. However, fully testing the integrity constraints after...
Ecological Partial Deduction: Preserving Characteristic Trees Without Constraints (1995)
. 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...
An almost perfect abstraction operator for partial deduction (1994)
Michael Leuschel, Danny De Schreye
A partial deduction strategy for logic programs usually uses an abstraction operator to guarantee the finiteness of the set of goals for which partial deductions are produced. Finding an abstraction...
Conjunctive Partial Deduction: Foundations, Control, Algorithms, And Experiments (1994)
Danny De Schreye, Robert Glück, Jesper Jørgensen, Robert Gl Uck, Michael Leuschel, Morten Heine Sørensen, ...
ion Operators We now specify the abstraction operators Abs fl;L , deciding which conjunctions are added to the global tree in order to ensure coveredness for bodies of newly derived resultants....
Partial Evaluation of the "Real Thing" (1994)
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...
The ECCE Partial Deduction System
Interpretation ". Most parts of the ecce system grew out of joint work with D. De Schreye, R. Gluck, J. Jørgensen, B. Martens, M.H. Sørensen and A. de Waal. I am also grateful to Wim Vanhoof,...