Prof. Dr. Michael Leuschel

Team Leuschel2.jpg

Contact Information

Heinrich-Heine-Universität Düsseldorf
Institut für Informatik
Universitätsstraße 1
D-40225 Düsseldorf

Email: leuschel@cs.uni-duesseldorf.de


Phone: +49 (211) 81-10710
Fax: +49 (211) 81-10712

Room: 25.12.02.60


Publications

2014
John Witulski, Michael Leuschel
Checking Computations of Formal Method Tools - A Secondary Toolchain for ProB [PDF] [Bibtex]
In Proceedings of the 1st Workshop on Formal-IDE, EPTCS XYZ, 2014, Electronic Proceedings in Theoretical Computer Science, 2014.
Who watches the watchers: Validating the ProB Validation Tool [PDF] [Bibtex]
In Proceedings of the 1st Workshop on Formal-IDE, EPTCS XYZ, 2014, Electronic Proceedings in Theoretical Computer Science, 2014.
Dominik Hansen, Lukas Ladenberger, Harald Wiegard, Jens Bendisposto, Michael Leuschel
Validation of the ABZ Landing Gear System using ProB [PDF] [Bibtex]
In Submitted to ABZ 2014, 2014.
2013
Validation of Formal Models by Refinement Animation [PDF] [Bibtex]
Science of Computer Programming, 78(3): 272-292, 2013.
Jerome Falampin, Hung Le-Dang, Michael Leuschel, Mikael Mokrani, Daniel Plagge
Improving Railway Data Validation with ProB [PDF] [Bibtex]
In: Industrial Deployment of System Engineering Methods, Springer: 27-44, 2013.
Sebastian Krings, Michael Leuschel
Inferring Physical Units in B Models [PDF] [Bibtex]
In Proceedings SEFM'2013, LNCS 8137, Springer, 2013.
B constrained [PDF] [Bibtex]
In Proceedings of the 4th Rodin User and Developer Workshop, TUCS Lecture Notes, TUCS, 2013.
Parallel Model Checking of B Specifications [PDF] [Bibtex]
In Proceedings of the 4th Rodin User and Developer Workshop, TUCS Lecture Notes, TUCS, 2013.
ProB 2.0 Tutorial [PDF] [Bibtex]
In Proceedings of the 4th Rodin User and Developer Workshop, TUCS Lecture Notes, TUCS, 2013.
Dominik Hansen, Michael Leuschel
Translating B to TLA+ for Validation with TLC [PDF] [Bibtex]
Technical Report, No. STUPS/2013/xx, Institut für Informatik, Heinrich-Heine-Universität Düsseldorf, 2013.
2012
Thierry Lecomte, Lilian Burdy, Michael Leuschel
Formally Checking Large Data Sets in the Railways [PDF] [Bibtex]
CoRR, abs/1210.6815, 2012.
Daniel Plagge, Michael Leuschel
Validating B, Z and TLA+ using ProB and Kodkod [PDF] [Bibtex]
In Proceedings FM'2012, LNCS 7436, Springer, 2012.
Dominik Hansen, Michael Leuschel
Translating TLA+ to B for Validation with ProB [PDF] [Bibtex]
In Proceedings iFM'2012, LNCS 7321, Springer, 2012.
2011
Michael Leuschel, Jérôme Falampin, Fabian Fritz, Daniel Plagge
Automated Property Verification for Large Scale B Models with ProB [PDF] [Bibtex]
Formal Aspects of Computing, 23(6): 683-709, 2011.
Stefan Hallerstede, Michael Leuschel
Constraint-Based Deadlock Checking of High-Level Specifications [PDF] [Bibtex]
Theory and Practice of Logic Programming, 11(4-5): 767-782, 2011.
Developing Camille, a text editor for Rodin [Bibtex]
Software: Practice and Experience, 41(2): 189-198, 2011.
Stefan Hallerstede, Michael Leuschel
Finding Deadlocks of Event-B Models by Constraint Solving [PDF] [Bibtex]
In B2011 Workshop (short paper), 2011.
Rainer Gmehlich, Katrin Grau, Stefan Hallerstede, Michael Leuschel, Felix Lösch, Daniel Plagge
On Fitting a Formal Method into Practice [PDF] [Bibtex]
In Proceedings ICFEM'2011, volume 6991 of Lecture Notes in Computer Science, Springer, 2011.
Jens Bendisposto, Michael Leuschel
Automatic Flow Analysis for Event-B [PDF] [Bibtex]
In Proceedings of Fundamental Approaches to Software Engineering (FASE) 2011, volume 6603 of Lecture Notes in Computer Science, Springer, 2011.
Carl Friedrich Bolz, Antonio Cuni, Maciej Fijałkowski, Michael Leuschel, Samuele Pedroni, Armin Rigo
Runtime Feedback in a Meta-Tracing JIT for Efficient Dynamic Languages [PDF] [Bibtex]
In Proceedings of the 6th workshop on the Implementation, Compilation, Optimization of Object-Oriented Languages and Programming Systems series = ICOOOLPS '11, 2011.
Carl Friedrich Bolz, Antonio Cuni, Maciej Fijałkowski, Michael Leuschel, Samuele Pedroni, Armin Rigo
Allocation removal by partial evaluation in a tracing JIT [PDF] [Bibtex]
In PEPM, 2011.
2010
Michael Leuschel, Thierry Massart
Efficient Approximate Verification of B via Symmetry Markers [PDF] [Bibtex]
Annals of Mathematics and Artificial Intelligence, 59(1): 81-106, 2010.
Daniel Plagge, Michael Leuschel
Seven at one stroke: LTL model checking for High-level Specifications in B, Z, CSP, and more [PDF] [Bibtex]
Software Tools for Technology Transfer (STTT), 12(1): 9-21, 2010.
Jitting Prolog for Fun and Profit [PDF] [Bibtex]
In DYLA 2010 - 4th Workshop on Dynamic Languages and Applications, 2010.
Towards a Jitting VM for Prolog Execution [PDF] [Bibtex]
In PPDP '10 - Proceedings of the 12th international ACM SIGPLAN symposium on Principles and practice of declarative programming, ACM, 2010.
Edd Turner, Michael Butler, Michael Leuschel
A Refinement-Based Correctness Proof of Symmetry Reduced Model Checking [PDF] [Bibtex]
In Proceedings ABZ'2010, volume 5977 of Lecture Notes in Computer Science, Springer-Verlag, 2010.
Refinement-Animation for Event-B - Towards a Method of Validation [PDF] [Bibtex]
In Proceedings ABZ'2010, volume 5977 of Lecture Notes in Computer Science, Springer-Verlag, 2010.
Michael Leuschel, Salvador Tamarit, Germán Vidal
Fast and Accurate Strong Termination Analysis with an Application to Partial Evaluation [PDF] [Bibtex]
In Proceedings WFLP'2009, LNCS 5979, Springer-Verlag, 2010.
Michael Leuschel, Jens Bendisposto
Directed Model Checking for B: An Evaluation and New Techniques [PDF] [Bibtex]
In SBMF'2010, volume 6527 of Lecture Notes in Computer Science, Springer, 2010.
Michael Jastram, Stefan Hallerstede, Michael Leuschel, Aryldo G Russo Jr
An Approach of Requirements Tracing in Formal Refinement [PDF] [Bibtex]
In VSTTE, volume 6217 of Lecture Notes in Computer Science, Springer, 2010.
Jens Bendisposto, Michael Leuschel, Markus Borgermans
GEPAVAS Gerichtete und parallele Validierung von abstrakten Spezifikationen - Projektreport [PDF] [Bibtex]
Technical Report, University of Düsseldorf, 2010.
2009
Michael Leuschel, Dominique Cansell, Michael Butler
Validating and Animating Higher-Order Recursive Functions in B [PDF] [Bibtex]
In Festschrift for Egon Börger, volume 5115 of Lecture Notes in Computer Science, Springer-Verlag, 2009.
Carl Friedrich Bolz, Michael Leuschel, Armin Rigo
Towards Just-In-Time Partial Evaluation of Prolog [PDF] [Bibtex]
In Logic-Based Program Synthesis and Transformation, 19th International Symposium, LOPSTR 2009, Coimbra, Portugal, September 2009, Revised Selected Papers, volume 6037 of Lecture Notes in Computer Science, Springer, 2009.
Michael Leuschel, Marisa Llorens, Javier Olivier, Josep Silva, Salvador Tamarit
SOC: A Slicer for CSP Specifications [Bibtex]
In PEPM 2009, ACM Press, 2009.
Daniel Plagge, Michael Leuschel, Ilya Lopatkin, Alexander Romanovsky
SAL, Kodkod, and BDDs for Validation of B Models. Lessons and Outlook [PDF] [Bibtex]
In Proceedings AFM 2009, 2009.
Michael Leuschel, Jérôme Falampin, Fabian Fritz, Daniel Plagge
Automated Property Verification for Large Scale B Models [PDF] [Bibtex]
In Proceedings FM 2009, volume 5850 of Lecture Notes in Computer Science, Springer-Verlag, 2009.
Mireille Samia, Michael Leuschel
Pie Tree Visualization [Bibtex]
In Proceedings SEKE, Knowledge Systems Institute, 2009.
Sebastian Wieczorek, Vitaly Kozyura, Andreas Roth, Michael Leuschel, Jens Bendisposto, Daniel Plagge, Ina Schieferdecker
Applying Model Checking to Generate Model-based Integration Tests from Choreography Models [PDF] [Bibtex]
In Proceedings TESTCOM/FATES 2009, volume 5826 of Lecture Notes in Computer Science, Springer-Verlag, 2009.
Mireille Samia, Harald Wiegard, Jens Bendisposto, Michael Leuschel
High-Level versus Low-Level Specifications: Comparing B with Promela and ProB with Spin [PDF] [Bibtex]
In Proceedings TFM-B 2009, APCB, 2009.
Visualising Event-B Models with B-Motion Studio [PDF] [Bibtex]
In Proceedings of FMICS 2009, volume 5825 of Lecture Notes in Computer Science, Springer, 2009.
Jens Bendisposto, Michael Leuschel
Proof Assisted Model Checking for B [PDF] [Bibtex]
In Proceedings of ICFEM 2009, volume 5885 of Lecture Notes in Computer Science, Springer, 2009.
Stefan Hallerstede, Michael Leuschel
How to explain mistakes [PDF] [Bibtex]
In TFM 2009, Lecture Notes in Computer Science, Springer-Verlag, 2009.
Jens Bendisposto, Michael Leuschel
Parallel Model Checking of Event-B Specification with ProB [Bibtex]
Work in Progress Report at PDMC 2009, http://www.pdmc.cz/PDMC09/accepted-papers.shtml, 2009.
2008
Steve Barker, Michael Leuschel, Mauricio Varea
Efficient and Flexible Access Control via Jones-Optimal Logic Program Specialisation [PDF] [Bibtex]
Higher-Order and Symbolic Computation, 21(1-2): 5-35, 2008.
Jens Bendisposto, Michael Leuschel, O. Ligot, Mireille Samia
La validation de modèles Event-B avec le plug-in ProB pour RODIN [Bibtex]
Technique et Science Informatiques, 27(8): 1065-1084, 2008.
Michael Leuschel, Marc Fontaine
Probing the Depths of CSP-M: A new FDR-compliant Validation Tool [PDF] [Bibtex]
ICFEM 2008, 2008.
Michael Leuschel, Michael Butler
ProB: An Automated Analysis Toolset for the B Method [PDF] [Bibtex]
Software Tools for Technology Transfer (STTT), 10(2): 185-203, 2008.
Michael Leuschel
The High Road to Formal Validation: Model Checking High-Level versus Low-Level Specifications [PDF] [Bibtex]
In ABZ 2008, volume 5238 of Lecture Notes in Computer Science, Springer-Verlag, 2008.
Michael Leuschel, Marisa Llorens, Javier Olivier, Josep Silva, Salvador Tamarit
Static Slicing of CSP Specifications [PDF] [Bibtex]
In Preproceedings LOPSTR'08, volume 5438 of Lecture Notes in Computer Science, 2008.
Michael Leuschel, Germán Vidal
Fast Offline Partial Evaluation for Large Logic Programs [PDF] [Bibtex]
In Proceedings LOPSTR'08, volume 5438 of Lecture Notes in Computer Science, 2008.
Michael Leuschel
Declarative Programming for Verification: Lessons and Outlook [PDF] [Bibtex]
In Proceedings PPDP'2008, ACM Press, 2008.
Corinna Spermann, Michael Leuschel
ProB gets Nauty: Effective Symmetry Reduction for B and Z Models [PDF] [Bibtex]
In Proceedings TASE 2008, IEEE, 2008.
Jens Bendisposto, Ian Endrijautzki, Michael Leuschel, David Schneider
A Semantics-Aware Editing Environment for Prolog in Eclipse [PDF] [Bibtex]
In Proceedings of the 18th Workshop on Logic-based methods in Programming Environments, WLPE, 2008.
Michael Leuschel, Mireille Samia, Jens Bendisposto, Li Luo
Easy Graphical Animation and Formula Viewing for Teaching B [PDF] [Bibtex]
In The B Method: from Research to Teaching, Lina, 2008.
2007
Olivier Ligot, Jens Bendisposto, Michael Leuschel
Debugging Event-B Models using the ProB Disprover Plug-in [PDF] [Bibtex]
Proceedings AFADL'07, 2007.
Dragan Bosnacki, Alastair F. Donaldson, Michael Leuschel, Thierry Massart
Efficient Approximate Verification of Promela Models via Symmetry Markers [PDF] [Bibtex]
In ATVA, volume 4762 of Lecture Notes in Computer Science, Springer-Verlag, 2007.
Michael Leuschel, Daniel Plagge
Seven at one stroke: LTL model checking for High-level Specifications in B, Z, CSP, and more [Bibtex]
In ISoLA, volume RNTI-SM-1 of Revue des Nouvelles Technologies de l'Information, 2007.
Daniel Plagge, Michael Leuschel
Validating Z Specifications using the ProB Animator and Model Checker [PDF] [Bibtex]
In Integrated Formal Methods, volume 4591 of Lecture Notes in Computer Science, Springer-Verlag, 2007.
Karl Klose, Klaus Ostermann, Michael Leuschel
Partial Evaluation of Pointcuts [PDF] [Bibtex]
In Practical Applications of Declarative Languages (PADL'07), Lecture Notes in Computer Science, Springer-Verlag, 2007.
Michael Leuschel, Michael Butler, Corinna Spermann, Edd Turner
Symmetry Reduction for B by Permutation Flooding [PDF] [Bibtex]
In Proceedings B'2007, volume 4355 of Lecture Notes in Computer Science, Springer-Verlag, 2007.
Michael Leuschel, Thierry Massart
Efficient Approximate Verification of B via Symmetry Markers [PDF] [Bibtex]
In Proceedings International Symmetry Conference, 2007.
Edd Turner, Michael Leuschel, Corinna Spermann, Michael Butler
Symmetry Reduced Model Checking for B [PDF] [Bibtex]
In Proceedings TASE 2007, IEEE, 2007.
Jens Bendisposto, Michael Leuschel
A Generic Flash-Based Animation Engine for ProB [PDF] [Bibtex]
In Proceedings of B 2007, volume 4355 of Lecture Notes in Computer Science, Springer, 2007.
Jens Bendisposto, Michael Leuschel
BE4: The B Extensible Eclipse Editing Environment [PDF] [Bibtex]
In Proceedings of B 2007, volume 4355 of Lecture Notes in Computer Science, Springer, 2007.
Manoranjan Satpathy, Michael Butler, Michael Leuschel, S. Ramesh
Automatic Testing from Formal Specifications [Bibtex]
In Tests and Proofs (TAP 2007), volume 4454 of Lecture Notes in Computer Science, Springer-Verlag, 2007.
Michael Leuschel, Daniel Plagge
Seven at one stroke: LTL model checking for High-level Specifications in B, Z, CSP, and more [PDF] [Bibtex]
Technical Report, No. STUPS/2007/02, Institut für Informatik, Heinrich-Heine-Universität Düsseldorf, 2007.
2006
Stephane Lo Presti, Michael Butler, Michael Leuschel, Chris Booth
Holistic Trust Design of E-Services [Bibtex]
In Ronggong Song, Larry Korba, George Yee (ed.): Trust in E-services: Technologies, Practices and Challenges, IGI Global: 113-139, 2006.
Michael Leuschel, Jens Bendisposto
Animating and Model Checking B Specifications with Higher-Order Recursive Functions [PDF] [Bibtex]
In Dagstuhl Seminar 06191 "Rigorous Methods for Software Construction and Analysis", 2006.
Michael Leuschel, Stephen Craig, Daniel Elphick
Supervising Offline Partial Evaluation of Logic Programs using Online Techniques [PDF] [Bibtex]
In Proceedings LOPSTR'06, volume 4407 of Lecture Notes in Computer Science, Springer-Verlag, 2006.
Michael Leuschel, Daniel Elphick, Mauricio Varea, Stephen Craig, Marc Fontaine
The Ecce and Logen Partial Evaluators and their Web Interfaces [PDF] [Bibtex]
In Proceedings PEPM 06, IBM Press, 2006.
2005
Michael Leuschel
Guest Editorial - Special Issue on Automated Verification of Critical Systems [Bibtex]
Formal Aspects of Computing, 17(2): 91-92, 2005.
Manoranjan Satpathy, Michael Leuschel, Michael Butler
ProTest: An Automatic Test Environment for B Specifications [PDF] [Bibtex]
Electronic Notes in Theroretical Computer Science, 111: 113-136, 2005.
Michael Butler, Michael Leuschel, Colin Snook
Tools for system validation with B abstract machines [PDF] [Bibtex]
In 12th International Workshop on Abstract State Machines, 2005.
Michael Leuschel, Germán Vidal
Forward Slicing by Conjunctive Partial Deduction and Argument Filtering [PDF] [Bibtex]
In ESOP, volume 3444 of Lecture Notes in Computer Science, Springer-Verlag, 2005.
Michael Leuschel, Michael Butler
Combining CSP and B for Specification and Property Verification [PDF] [Bibtex]
In FM'2005, volume 3582 of Lecture Notes in Computer Science, Springer-Verlag, 2005.
Qian Wang, Gopal Gupta, Michael Leuschel
Towards Provably Correct Code Generation via Horn Logical Continuation Semantics [PDF] [Bibtex]
In PADL, volume 3350 of Lecture Notes in Computer Science, Springer-Verlag, 2005.
Michael Leuschel, Stephen Craig
A Reconstruction of the Lloyd-Topor Transformation using Partial Evaluation [PDF] [Bibtex]
In Pre-Proceedings of LOPSTR'05, 2005.
Michael Leuschel, Michael Butler
Automatic Refinement Checking for B [PDF] [Bibtex]
In Proceedings ICFEM, volume 3785 of Lecture Notes in Computer Science, Springer-Verlag, 2005.
Stephen Craig, Michael Leuschel
Self-Tuning Resource Aware Specialisation for Prolog [PDF] [Bibtex]
In Proceedings PPDP'2005, ACM Press, 2005.
Stephane Lo Presti, Michael Butler, Michael Leuschel, Chris Booth
A Trust Analysis Methodology for Pervasive Computing Systems [PDF] [Bibtex]
In Trusting Agents for trusting Electronic Societies, volume 3577 of Lecture Notes in Computer Science, Springer-Verlag, 2005.
Michael Leuschel, Edd Turner
Visualising Larger State Spaces in ProB [PDF] [Bibtex]
In ZB, volume 3455 of Lecture Notes in Computer Science, Springer-Verlag, 2005.
2004
Michael Leuschel
A Framework for the Integration of Partial Evaluation and Abstract Interpretation of Logic Programs [PDF] [Bibtex]
ACM Transactions on Programming Languages and Systems (TOPLAS), 26(3): 413-463, 2004.
Michael Leuschel, Jesper Jørgensen, Wim Vanhoof, Maurice Bruynooghe
Offline Specialisation in Prolog Using a Hand-Written Compiler Generator [PDF] [Bibtex]
TPLP, 4(1-2): 139-191, 2004.
Stephen Craig, Michael Leuschel
Lix: An Effective Self-applicable Partial Evaluator for Prolog [PDF] [Bibtex]
In FLOPS, Springer-Verlag, 2004.
Michael Leuschel
ProB: Un outil de modélisation formelle (Invited Talk) [PDF] [Bibtex]
In JFPLC, Hermes Science Publications, Lavoisier, 2004.
Stephen Craig, John Gallagher, Michael Leuschel, Kim S. Henriksen
Fully Automatic Binding Time Analysis for Prolog [PDF] [Bibtex]
In LOPSTR, volume 3573 of Lecture Notes in Computer Science, Springer-Verlag, 2004.
Steve Barker, Michael Leuschel, Mauricio Varea
Efficient and Flexible Access Control via Logic Program Specialisation [PDF] [Bibtex]
In PEPM, ACM Press, 2004.
Berndt Farwer, Michael Leuschel
Model Checking of Object Petri Nets in Prolog [PDF] [Bibtex]
In PPDP, ACM Press, 2004.
Wim Vanhoof, Maurice Bruynooghe, Michael Leuschel
Binding-Time Analysis for Mercury [PDF] [Bibtex]
In Program Development in Computational Logic, volume 3049 of Lecture Notes in Computer Science, Springer-Verlag, 2004.
Michael Leuschel, Stephen Craig, Maurice Bruynooghe, Wim Vanhoof
Specializing Interpreters using Offline Partial Deduction [PDF] [Bibtex]
In Program Development in Computational Logic, volume 3049 of Lecture Notes in Computer Science, Springer-Verlag, 2004.
Michael Butler, Michael Leuschel, Stephane Lo Presti, Phillip Turner
The Use of Formal Methods in the Analysis of Trust (Position Paper) [Bibtex]
In iTrust, volume 2995 of Lecture Notes in Computer Science, Springer-Verlag, 2004.
Stephane Lo Presti, Michael Butler, Michael Leuschel, Colin Snook, Phillip Turner
Formal Modelling and Verification of Trust in a Pervasive Application [PDF] [Bibtex]
Technical Report, DSSE, University of Southampton, 2004.
Michael Leuschel, Edd Turner
Visualising Larger State Spaces in ProB [Bibtex]
Technical Report, ECS, University of Southampton, 2004.
2003
Michael Butler, Michael Leuschel, Stephane Lo Presti, David Allsopp, Patrick Beautement, Chris Booth, Mark Cusack, Mike Kirton
Towards a Trust Analysis Framework for Pervasive Computing Scenarios [PDF] [Bibtex]
IEEE Computing, 2(3), 2003.
Juan Carlos Augusto, Michael Leuschel, Michael Butler, Carla Ferreira
Using the Extensible Model Checker XTL to Verify StAC Business Specifications [PDF] [Bibtex]
In AVoCS, 2003.
Juan Carlos Augusto, Carla Ferreira, Andy M. Gravell, Michael Leuschel, Karen M.Y. Ng
The Benefits of Rapid Modelling for E-Business System Development [PDF] [Bibtex]
In ER (Workshops), volume 2814 of Lecture Notes in Computer Science, Springer Verlag, 2003.
Stephen Craig, Michael Leuschel
A Compiler Generator for Constraint Logic Programs [PDF] [Bibtex]
In Ershov Memorial Conference, volume 2890 of Lecture Notes in Computer Science, Springer-Verlag, 2003.
Michael Leuschel, Michael Butler
ProB: A Model Checker for B [PDF] [Bibtex]
In FME, volume 2805 of Lecture Notes in Computer Science, Springer-Verlag, 2003.
Daniel Elphick, Michael Leuschel, Simon Cox
Partial Evaluation of MATLAB [PDF] [Bibtex]
In GPCE, Lecture Notes in Computer Science, Springer-Verlag, 2003.
Helko Lehmann, Michael Leuschel
Inductive Theorem Proving by Program Specialisation: Generating proofs for Isabelle using Ecce (Invited talk) [PDF] [Bibtex]
In LOPSTR, volume 3018 of Lecture Notes in Computer Science, Springer-Verlag, 2003.
Mauricio Varea, Michael Leuschel, Bashir Al-Hashimi
Improving Compositional Verification of State-based Models by Reducing Modular Unbalance [PDF] [Bibtex]
In Refinement of Critical Systems, 2003.
Michael Leuschel, Stephen Craig, Maurice Bruynooghe, Wim Vanhoof
Specializing Interpreters using Offline Partial Deduction [PDF] [Bibtex]
Technical Report, No. DSSE-TR-2003-5, ECS, University of Southampton, 2003.
2002
Michael Leuschel, Maurice Bruynooghe
Logic program specialisation through partial deduction: Control Issues [PDF] [Bibtex]
Theory and Practice of Logic Programming, 2(4-5): 461-515, 2002.
Mauricio Varea, Bashir Al-Hashimi, Michael Leuschel
Finite and Infinite Model Checking of Dual Transition Petri Net Models [PDF] [Bibtex]
In AVoCS, 2002.
Michael Leuschel, Thierry Massart
Logic programming and partial deduction for the verification of reactive systems: An experimental evaluation [PDF] [Bibtex]
In AVoCS, University of Birmingham, 2002.
Michael Leuschel, Stefan Gruner
Abstract Conjunctive Partial Deduction using Regular Types and its Application to Model Checking [Bibtex]
In LOPSTR, volume 2372 of Lecture Notes in Computer Science, Springer-Verlag, 2002.
Michael Leuschel
Homeomorphic Embedding for Online Termination of Symbolic Methods [PDF] [Bibtex]
In The Essence of Computation - Essays dedicated to Neil Jones, volume 2566 of Lecture Notes in Computer Science, Springer-Verlag, 2002.
Helko Lehmann, Michael Leuschel
Generating inductive verification proofs for Isabelle using the partial evaluator Ecce [Bibtex]
Technical Report, No. DSSE-TR-2002-02, ECS, University of Southampton, 2002.
2001
Hugh Glaser, Pieter H. Hartel, Michael Leuschel, Andrew Martin
Declarative Languages in Education [PDF] [Bibtex]
Encyclopaedia of Microcomputers, 27: 79-102, 2001.
Michael Leuschel, Ivan Wolton, Thierry Massart, Laksono Adhianto
Temporal Logic Model Checking of CSP: Tools and Techniques [Bibtex]
In AVoCS 2001, Oxford University Computing Laboratory, 2001.
Michael Leuschel
Design and Implementation of the High-Level Specification Language CSP(LP) [PDF] [Bibtex]
In PADL, volume 1990 of Lecture Notes in Computer Science, Springer, 2001.
Michael Leuschel, Thierry Massart, Andrew Currie
How to make FDR Spin: LTL model checking of CSP using Refinement [PDF] [Bibtex]
In Proceedings FME'2001, Springer-Verlag, 2001.
Laksono Adhianto, Michael Leuschel
Strategy for Improving Memory Locality Reuse and Exploiting Hidden Parallelism [Bibtex]
In Proceedings of ISSM, 2001.
Michael Leuschel, Laksono Adhianto, Michael Butler, Carla Ferreira, Leonid Mikhailov
Animation and Model Checking of CSP and B using Prolog Technology [Bibtex]
In Proceedings of the ACM Sigplan Workshop on Verification and Computational Logic, 2001.
2000
Michael Leuschel, Helko Lehmann
Coverability of Reset Petri Nets and other Well-Structured Transition Systems by Partial Deduction [PDF] [Bibtex]
In Computational Logic, volume 1861 of Lecture Notes in Computer Science, 2000.
Helko Lehmann, Michael Leuschel
Decidability Results for the Propositional Fluent Calculus [Bibtex]
In Computational Logic, volume 1861 of Lecture Notes in Computer Science, Springer-Verlag, 2000.
Helko Lehmann, Michael Leuschel
Solving Planning Problems by Partial Deduction [PDF] [Bibtex]
In LPAR, volume 1955 of Lecture Notes in Computer Science, Springer-Verlag, 2000.
Michael Leuschel, Helko Lehmann
Solving Coverability Problems of Petri Nets by Partial Deduction [PDF] [Bibtex]
In PPDP, ACM Press, 2000.
Andrew Currie, Michael Leuschel, Thierry Massart
LTL Model Checking of CSP by Refinement: How to Make FDR Spin [Bibtex]
In Proceedings VCL'2000, 2000.
Michael Leuschel, Maurice Bruynooghe
Control Issues in Partial Deduction: The Ever Ending Story [Bibtex]
Technical Report, University of Southampton, 2000.
1999
Danny De Schreye, Robert Glueck, Jesper Jørgensen, Michael Leuschel, Bern Martens, Morten H. Sørensen
Conjunctive Partial Deduction: Foundations, Control, Algorithms, and Experiments [PDF] [Bibtex]
Journal of Logic Programming, 41(2-3): 231-277, 1999.
Michael Leuschel, Jesper Jørgensen
Efficient Specialisation in Prolog Using the Hand-Written Compiler Generator LOGEN [Bibtex]
Electronic Notes in Theoretical Computer Science, 30(2): 157-162, 1999.
Robert Glueck, Michael Leuschel
Abstraction-Based Partial Deduction for Solving Inverse Problems - A Transformational Approach to Software Verification [Bibtex]
In Ershov Memorial Conference, volume 1755 of Lecture Notes in Computer Science, Springer-Verlag, 1999.
Jonathan C. Martin, Michael Leuschel
Sonic Partial Deduction [Bibtex]
In Ershov Memorial Conference, volume 1755 of Lecture Notes in Computer Science, Springer-Verlag, 1999.
Michael Leuschel, Thierry Massart
Infinite State Model Checking by Abstract Interpretation and Program Specialisation [PDF] [Bibtex]
In LOPSTR '99, volume 1817 of Lecture Notes in Computer Science, Springer-Verlag, 1999.
Michael Leuschel
Advanced Logic Program Specialisation [PDF] [Bibtex]
In Partial Evaluation - Practice and Theory, DIKU 1998 International Summer School, Springer-Verlag, 1999.
Michael Leuschel
Logic Program Specialisation [PDF] [Bibtex]
In Partial Evaluation: Practice and Theory, volume 1706 of Lecture Notes in Computer Science, Springer-Verlag, 1999.
P. Hartel, Michael Butler, Andrew Currie, P. Henderson, Michael Leuschel, A. Martin, A. Smith, Ulrich Ultes-Nitsche, R.J. Walters
Questions and Answers About Ten Formal Methods [Bibtex]
In Proc. 4th Int. Workshop on Formal Methods for Industrial Critical Systems, STAR/CNR, Pisa, Italy, 1999.
Michael Leuschel, Nick Linnenbruegger, Jerome Thoma
Analyzing Context-Free and Context-Sensitive Grammars by Abstract Interpretation [Bibtex]
In Proceedings of the Formal Grammar Conference FG'99, University of Utrecht, 1999.
Michael Leuschel, Jesper Jørgensen
Efficient Specialisation in Prolog Using a Hand-Written Compiler Generator [Bibtex]
Technical Report, No. DSSE-TR-99-6, University of Southampton, 1999.
1998
Michael Leuschel, Danny De Schreye
Constrained Partial Deduction and the Preservation of Characteristic Trees [Bibtex]
New Generation Computing, 16(3): 283-342, 1998.
Michael Leuschel, Bern Martens, Danny De Schreye
Controlling Generalisation and Polyvariance in Partial Deduction of Normal Logic Programs [Bibtex]
ACM Transactions on Programming Languages and Systems, 20(1): 208-258, 1998.
Michael Leuschel, Danny De Schreye
Creating Specialised Integrity Checks Through Partial Evaluation of Meta-interpreters [PDF] [Bibtex]
Journal of Logic Programming, 36(2): 149-193, 1998.
Konstantinos Sagonas, Michael Leuschel
Extending Partial Deduction to Tabled Execution: Some Results and Open Issues [Bibtex]
ACM Computing Surveys, 30(3es), 1998.
Michael Leuschel, Bern Martens, Danny De Schreye
Some Achievements and Prospects in Partial Deduction [Bibtex]
ACM Computing Surveys, 30(3es), 1998.
Maurice Bruynooghe, Michael Leuschel, Konstantinos Sagonas
A Polyvariant Binding-Time Analysis for Off-line Partial Deduction [PDF] [Bibtex]
In ESOP, volume 1381 of Lecture Notes in Computer Science, Springer-Verlag, 1998.
Michael Leuschel
Program Specialisation and Abstract Interpretation Reconciled [PDF] [Bibtex]
In IJCSLP, MIT Press, 1998.
Michael Leuschel, Bern Martens, Konstantinos Sagonas
Preserving Termination of Tabled Logic Programs While Unfolding [PDF] [Bibtex]
In LOPSTR '97, volume 1463 of Lecture Notes in Computer Science, Springer-Verlag, 1998.
Stefaan Decorte, Danny De Schreye, Michael Leuschel, Bern Martens, Konstantinos Sagonas
Termination Analysis for Tabled Logic Programming [PDF] [Bibtex]
In LOPSTR '97, volume 1463 of Lecture Notes in Computer Science, Springer-Verlag, 1998.
Michael Leuschel
Improving Homeomorphic Embedding for Online Termination [PDF] [Bibtex]
In LOPSTR '98, volume 1559 of Lecture Notes in Computer Science, Springer-Verlag, 1998.
Michael Leuschel
On the Power of Homeomorphic Embedding for Online Termination [PDF] [Bibtex]
In Proceedings SAS, volume 1503 of Lecture Notes in Computer Science, Springer-Verlag, 1998.
1997
Michael Leuschel
Advanced Techniques for Logic Program Specialisation [Bibtex]
AI Communications, 10(2): 127-128, 1997.
Michael Leuschel
Specialization of Declarative Programs and its Application (workshop overview) [Bibtex]
In ILPS, MIT Press, 1997.
Michael Leuschel
The Ecce Partial Deduction System [Bibtex]
In Proceedings of the ILPS'97 Workshop on Tools and Environments for (Constraint) Logic Programming, 1997.
Michael Leuschel
Advanced Techniques for Logic Program Specialisation [PDF] [Bibtex]
PhD Thesis, K.U. Leuven, 1997.
1996
Jesper Jørgensen, Michael Leuschel
Efficiently Generating Efficient Generating Extensions in Prolog [PDF] [Bibtex]
In Dagstuhl Seminar on Partial Evaluation, volume 1110 of Lecture Notes in Computer Science, Springer-Verlag, 1996.
Michael Leuschel, Bern Martens
Global Control for Partial Deduction through Characteristic Atoms and Global Trees [PDF] [Bibtex]
In Dagstuhl Seminar on Partial Evaluation, volume 1110 of Lecture Notes in Computer Science, Springer-Verlag, 1996.
Michael Leuschel, Danny De Schreye, D. Andre de Waal
A Conceptual Embedding of Folding into Partial Deduction: Towards a Maximal Integration [PDF] [Bibtex]
In JICSLP, MIT Press, 1996.
Jesper Jørgensen, Michael Leuschel, Bern Martens
Conjunctive Partial Deduction in Practice [PDF] [Bibtex]
In LOPSTR, volume 1207 of Lecture Notes in Computer Science, Springer-Verlag, 1996.
Michael Leuschel, Danny De Schreye
Logic Program Specialisation: How To Be More Specific (abstract) [Bibtex]
In LOPSTR, volume 1207 of Lecture Notes in Computer Science, Springer-Verlag, 1996.
Michael Leuschel, Morten Heine Sørensen
Redundant Argument Filtering of Logic Programs [Bibtex]
In LOPSTR, volume 1207 of Lecture Notes in Computer Science, Springer-Verlag, 1996.
Michael Leuschel
Specialised Integrity Checking by Combining Conjunctive Partial Deduction and Abstract Interpretation [Bibtex]
In Proc. Logic Databases and the Meaning of Change: Dagstuhl-Seminar-Report 157, IBFI GmbH, Schloss Dagstuhl, 1996.
Michael Leuschel, Danny De Schreye
Logic Program Specialisation: How To Be More Specific [PDF] [Bibtex]
In Proceedings PLILP'96, volume 1140 of Lecture Notes in Computer Science, Springer-Verlag, 1996.
1995
Michael Leuschel, Bern Martens
Partial Deduction of the Ground Representation and its Application to Integrity Checking [Bibtex]
In ILPS, MIT Press, 1995.
Michael Leuschel, Danny De Schreye, Bern Martens
Tutorial on Program Specialisation (abstract) [Bibtex]
In ILPS, MIT Press, 1995.
Michael Leuschel, Danny De Schreye
Towards Creating Specialised Integrity Checks Through Partial Evaluation of Meta-Interpreters [PDF] [Bibtex]
In PEPM, ACM Press, 1995.
Michael Leuschel, Bern Martens
Obtaining Specialised Update Procedures through Partial Deduction of the Ground Representation [Bibtex]
In Proc. Joint Workshop on Deductive Databases and Logic Programming and Abduction in Deductive Databases and Knowledge Based Systems, GMD-Studien Nr. 266, 1995.
1994
Michael Leuschel
Partial Evaluation of the "Real Thing" [Bibtex]
In LOPSTR, volume 883 of Lecture Notes in Computer Science, Springer-Verlag, 1994.