2025

Timo Strobel, Wolfgang-Reza Sharavi, Sadegh Sadeghipour, Nicolas Grube, Michael Leuschel, Jan Gruteser, Jan Roßbach, Oliver De Candido, Anja Philippsen, Dorian Knoblauch
KI-LOK – a joint project involving test procedures for AI-based components in railway operations.
In SIGNALLING & DATACOMMUNICATION, 29--37, 2025.
- LINK

2024

Jan Roßbach, Oliver De Candido, Ahmed Hammam, Michael Leuschel
Evaluating AI-Based Components in Autonomous Railway Systems.
In Proceedings KI 2024, LNAI, 14992, Springer, 190--203, 2024.
- The final authenticated version is available online at https://doi.org/10.1007/978-3-031-70893-0_14
Fabian Vu, Jannik Dunkelau, Michael Leuschel
Validation of Reinforcement Learning Agents and Safety Shields with ProB.
In Proceedings NFM 2024, LNCS, 14627, Springer, 279--297, 2024.
- The final authenticated version is available online at https://doi.org/10.1007/978-3-031-60698-4_16
Jan Gruteser, Michael Leuschel
Validation of railML Using ProB.
In Proceedings ICECCS 2024, LNCS, 14784, Springer, 245--256, 2024.
- The final authenticated version is available online at https://doi.org/10.1007/978-3-031-66456-4_13
Fabian Vu, Christopher Happe, Michael Leuschel
Generating interactive documents for domain-specific validation of formal models.
In International Journal on Software Tools for Technology Transfer, 26, 2, Springer, 147--168, 2024.
- The final authenticated version is available online at https://doi.org/10.1007/s10009-024-00739-0
Michael Leuschel, Jan Gruteser
Real Animation of TLA+ Models.
In TLA+ Community Event, 2024.
- PDF
Jan Gruteser, Jan Roßbach, Fabian Vu, Michael Leuschel
Using Formal Models, Safety Shields and Certified Control to Validate AI-Based Train Systems.
In Proceedings FMAS 2024, EPTCS, 411, 151--159, 2024.
- The final authenticated version is available online at https://doi.org/10.4204/EPTCS.411.10
Michael Leuschel, Jan Gruteser, Jan Roßbach
Prüfverfahren für KI-basierte Komponenten im Eisenbahnbetrieb (KI-LOK).
Technical Report, Heinrich-Heine-Universität Düsseldorf, HHU-STUPS 2024-12-1, 2024.
- PDF
- LINK

2023

Fabian Vu, Michael Leuschel
Validation of Formal Models by Interactive Simulation.
In Proceedings ABZ 2023, LNCS, 14010, Springer, 59--69, 2023.
- The final authenticated version is available online at https://doi.org/10.1007/978-3-031-33163-3_5
Sebastian Stock, Fabian Vu, David Geleßus, Michael Leuschel, Atif Mashkoor, Alexander Egyed
Validation by Abstraction and Refinement.
In Proceedings ABZ 2023, LNCS, 14010, Springer, 160--178, 2023.
- The final authenticated version is available online at https://doi.org/10.1007/978-3-031-33163-3_12
David Geleßus, Sebastian Stock, Fabian Vu, Michael Leuschel, Atif Mashkoor
Modeling and Analysis of a Safety-Critical Interactive System Through Validation Obligations.
In Proceedings ABZ 2023, LNCS, 14010, Springer, 284--302, 2023.
- The final authenticated version is available online at https://doi.org/10.1007/978-3-031-33163-3_22
Sophia Reinhardt, Joshua Schmidt, Jonas Schneider, Elena Schulte, Christiane Schüle, Michael Leuschel, Jörg Schipper
Smartphone-Based Videonystagmography Using Artificial Intelligence.
In Current Directions in Biomedical Engineering, 9, 1, 528--531, 2023.
- LINK
Jannik Dunkelau, Michael Leuschel
Performance Fuzzing with Reinforcement-Learning and Well-Defined Constraints for the B Method.
In iFM 2023, Springer, 237--256, 2023.
- PDF
- The final authenticated version is available online at https://link.springer.com/chapter/10.1007/978-3-031-47705-8_13
Jan Gruteser, David Geleßus, Michael Leuschel, Jan Roßbach, Fabian Vu
A Formal Model of Train Control with AI-Based Obstacle Detection.
In Proceedings RSSRail 2023, Birgit Milius and Simon Collart Dutilleul and Thierry Lecomte, LNCS, 14198, Springer, 128--145, 2023.
- The final authenticated version is available online at https://doi.org/10.1007/978-3-031-43366-5_8
Jan Roßbach, Michael Leuschel
Certified Control for Train Sign Classification.
In Proceedings FMAS 2023, Marie Farrell and Matt Luckcuck and Mario Gleirscher and Maike Schwammberger, EPTCS, 395, 69--76, 2023.
- The final authenticated version is available online at https://doi.org/10.4204/EPTCS.395.5

2022

Fabian Vu, Christopher Happe, Michael Leuschel
Generating Domain-Specific Interactive Validation Documents.
In Proceedings FMICS, LNCS, 13487, Springer, 32--49, 2022.
- The final authenticated version is available online at https://doi.org/10.1007/978-3-031-15008-1_4
Fabian Vu, Dominik Brandt, Michael Leuschel
Model Checking B Models via High-Level Code Generation.
In Proceedings ICFEM, LNCS, 13478, Springer, 334--351, 2022.
- The final authenticated version is available online at https://doi.org/10.1007/978-3-031-17244-1_20
Sophia Reinhardt, Joshua Schmidt, Jonas Schneider, Michael Leuschel, Christiane Schüle, Jörg Schipper
VertiGo-App - Smartphone-based video nystagmography using artificial intelligence.
In Laryngorhinootologie 2022, 101, 2, 243--244, 2022.
- LINK
Joshua Schmidt, Michael Leuschel
SMT solving for the validation of B and Event-B models.
In Software Tools for Technology Transfer (STTT), Springer-Verlag, 2022.
Philipp Körner, Michael Leuschel, João Barbosa, Vtor Santos Costa, Verónica Dahl, Manuel V. Hermenegildo, José F. Morales, Jan Wielemaker, Daniel Diaz, Salvador Abreu
Fifty Years of Prolog and Beyond.
In Theory and Practice of Logic Programming, 22, 6, 776--858, 2022.
- The final authenticated version is available online at https://doi.org/10.1017/S1471068422000102
Philipp Körner, Michael Leuschel
Towards Practical Partial Order Reduction for High-Level Formalisms.
In Verified Software. Theories, Tools and Experiments - 14th International Conference, VSTTE 2022, Trento, Italy, October 17-18, 2022, Revised Selected Papers, Lecture Notes in Computer Science, 13800, Springer, 72--91, 2022.
- PDF
- The final authenticated version is available online at https://doi.org/10.1007/978-3-031-25803-9_5

2021

Fabian Vu, Michael Leuschel, Atif Mashkoor
Validation of Formal Models by Timed Probabilistic Simulation.
In Proceedings ABZ, LNCS, 12709, Springer, 81--96, 2021.
- The final authenticated version is available online at https://doi.org/10.1007/978-3-030-77543-8_6
Jens Bendisposto, David Geleßus, Yumiko Jansing, Michael Leuschel, Antonia Pütz, Fabian Vu, Michelle Werth
ProB2-UI: A Java-Based User Interface for ProB.
In Proceedings FMICS, LNCS, 12863, Springer, 193--201, 2021.
- The final authenticated version is available online at https://doi.org/10.1007/978-3-030-85248-1_12
Philipp Körner, David Schneider, Michael Leuschel
On the Performance of Bytecode Interpreters in Prolog.
In Proceedings WFLP 2020, LNCS, 12560, Springer, 2021.
- PDF
Joshua Schmidt, Michael Leuschel
Improving SMT Solver Integrations for the Validation of B and Event-B Models.
In Formal Methods for Industrial Critical Systems, Alberto Lluch Lafuente and Anastasia Mavridou, LNCS, 12863, Springer International Publishing, 107--125, 2021.
- The final authenticated version is available online at https://doi.org/10.1007/978-3-030-85248-1_7

2020

Sebastian Krings, Michael Leuschel, Joshua Schmidt, David Schneider, Marc Frappier
Translating Alloy and extensions to classical B.
In Science of Computer Programming, 188, 2020.
Dominik Hansen, Michael Leuschel, Philipp Körner, Sebastian Krings, Thomas Naulin, Nader Nayeri, David Schneider, Frank Skowron
Validation and real-life demonstration of ETCS hybrid level 3 principles using a formal B model.
In International Journal on Software Tools for Technology Transfer, 2020.
- LINK
Philipp Körner, Michael Leuschel, Jannik Dunkelau
Towards a Shared Specification Repository.
In Proceedings ABZ, LNCS, 12071, Springer, 2020.
- PDF
- The final authenticated version is available online at https://link.springer.com/chapter/10.1007/978-3-030-48077-6_22
Jannik Dunkelau, Joshua Schmidt, Michael Leuschel
Analysing ProB’s Constraint Solving Backends.
In Proceedings ABZ, LNCS, 12071, Springer, 107--123, 2020.
- PDF
- The final authenticated version is available online at https://doi.org/10.1007/978-3-030-48077-6_8
Michelle Werth, Michael Leuschel
VisB: A Lightweight Tool to Visualize Formal Models with SVG Graphics.
In Proceedings ABZ, LNCS, 12071, Springer, 260--265, 2020.
- The final authenticated version is available online at https://doi.org/10.1007/978-3-030-48077-6_21
Sophia Reinhardt, Joshua Schmidt, Michael Leuschel, Christiane Schüle, Jörg Schipper
VertiGo - Pilot project for nystagmus detection via webcam.
In Laryngo-Rhino-Otologie, 99, Thieme Verlag, 2020.
- LINK
Philipp Körner, David Schneider, Michael Leuschel
On the Performance of Bytecode Interpreters in Prolog.
In Pre-Proceedings WFLP, 2020.
Michael Butler, Philipp Körner, Sebastian Krings, Thierry Lecomte, Michael Leuschel, Luis-Fernando Mejia, Laurent Voisin
The First Twenty-Five Years of Industrial Use of the B Method.
In Proceedings FMICS, LNCS, 12327, Springer, 2020.
- PDF
Philipp Körner, Jens Bendisposto, Jannik Dunkelau, Sebastian Krings, Michael Leuschel
Integrating formal specifications into applications: the ProB Java API.
In Formal Methods in System Design, Springer, 2020.
- LINK
Sophia Reinhardt, Joshua Schmidt, Michael Leuschel, Christiane Schüle, Jörg Schipper
VertiGo – a pilot project in nystagmus detection via webcam.
In Current Directions in Biomedical Engineering , 6, De Gruyter, 2020.
- LINK

2019

Jannik Dunkelau, Michael Leuschel
Fairness-Aware Machine Learning: An Extensive Overview.
Unpublished, 2019.
- PDF
Philipp Körner, Jens Bendisposto, Jannik Dunkelau, Sebastian Krings, Michael Leuschel
Embedding High-Level Formal Specifications into Applications.
In Proceedings FM, LNCS, 11800, Springer, 2019.
- PDF
- The final authenticated version is available online at https://doi.org/10.1007/978-3-030-30942-8_31
Sebastian Krings, Michael Butler, Philipp Körner, Thierry Lecomte, Michael Leuschel, Laurent Voisin
The History and Evolution of B and Event-B.
In Presentation HFM, 2019.
- PDF
Fabian Vu, Dominik Hansen, Philipp Körner, Michael Leuschel
A Multi-Target Code Generator for High-Level B.
In Proceedings iFM, LNCS, 11918, Springer, 2019.
- PDF
- The final authenticated version is available online at https://doi.org/10.1007/978-3-030-34968-4_25

2018

Sebastian Krings, Michael Leuschel
Proof Assisted Bounded and Unbounded Symbolic Model Checking of Software and System Models.
In Science of Computer Programming, 158, 41-63, 2018.
Sebastian Krings, Michael Leuschel, Philipp Körner, Stefan Hallerstede, Miran Hasanagic
Three is a crowd: SAT, SMT and CLP on a chessboard.
In Proceedings PADL 2018, LNCS, 10702, Springer, 2018.
- PDF
- The final authenticated version is available online at https://doi.org/10.1007/978-3-319-73305-0_5
Philipp Körner, Jeroen Meijer, Michael Leuschel
State-of-the-Art Model Checking for B and Event-B Using ProB and LTSmin.
In Proceedings iFM 2018, LNCS, 11023, Springer, 2018.
- PDF
- The final authenticated version is available online at https://doi.org/10.1007/978-3-319-98938-9_16
Dominik Hansen, Michael Leuschel, David Schneider, Sebastian Krings, Philipp Körner, Thomas Naulin, Nader Nayeri, Frank Skowron
Using a Formal B Model at Runtime in a Demonstration of the ETCS Hybrid Level 3 Concept with Real Trains.
In Proceedings ABZ 2018, Michael Butler and Alexander Raschke and Thai Son Hoang and Klaus Reichl, LNCS, 10817, Springer, 292--306, 2018.
- PDF
- The final authenticated version is available online at https://doi.org/10.1007/978-3-319-91271-4_20
Sebastian Krings, Joshua Schmidt, Carola Brings, Marc Frappier, Michael Leuschel
A Translation from Alloy to B.
In Proceedings ABZ 2018, LNCS, 10817, Springer, 71--86, 2018.
- PDF
Joshua Schmidt, Sebastian Krings, Michael Leuschel
Repair and Generation of Formal Models Using Synthesis.
In Proceedings iFM 2018, LNCS, 11023, Springer, 2018.
Schneider, David, Leuschel, Michael, Witt, Tobias
Model-based problem solving for university timetable validation and improvement.
In Formal Aspects of Computing, 2018.
- LINK
Philipp Körner, Michael Leuschel
Embedding Formal Specifications as Libraries into Applications.
Technical Report, School of Computing, Newcastle University, 1525, 2018.
- LINK

2016

Sebastian Krings, Michael Leuschel
Constraint Logic Programming over Infinite Domains with an Application to Proof.
In Proceedings of the 30th Workshop on (Constraint) Logic Programming, EPTCS, 234, 2016.
- PDF
Ivaylo Dobrikov, Michael Leuschel
Optimising the ProB Model Checker for B using partial order reduction.
In Formal Aspects of Computing, 28, 2, 179--323, 2016.
- PDF
- LINK
Sebastian Krings, Michael Leuschel
Proof Assisted Symbolic Model Checking for B and Event-B.
In Proceedings ABZ 2016, LNCS, 9675, Springer, 2016.
- PDF
Joshua Schmidt, Sebastian Krings, Michael Leuschel
Interactive Model Repair by Synthesis.
In Proceedings ABZ 2016, LNCS, 9675, Springer, 2016.
- PDF
Sebastian Krings, Michael Leuschel
SMT Solvers for Validation of B and Event-B models.
In Proceedings iFM 2016, LNCS, 9681, Springer, 2016.
- PDF
Jens Bendisposto, Philipp Körner, Michael Leuschel, Jeroen Meijer, van de Pol, Jaco, Helen Treharne, Jorden Whitefield
Symbolic Reachability Analysis of B through ProB and LTSmin.
In Proceedings iFM 2016, LNCS, 9681, Springer, 2016.
- PDF
- The final authenticated version is available online at https://doi.org/10.1007/978-3-319-33693-0_18
Ivaylo Dobrikov, Michael Leuschel
Enabling Analysis for Event-B.
In Proceedings ABZ 2016, LNCS, 9675, Springer, 2016.
- PDF
Dominik Hansen, David Schneider, Michael Leuschel
Using B and ProB for Data Validation Projects.
In Proceedings ABZ 2016, LNCS, 9675, Springer-Verlag, 2016.
Ivaylo Dobrikov, Michael Leuschel
Enabling Analysis for Event-B (Technical Report).
Technical Report, Institut für Informatik, University of Düsseldorf, STUPS/2016/xx, 2016.
- PDF
- LINK
Ivaylo Dobrikov, Daniel Plagge,, Michael Leuschel
LTL Model Checking under Fairness in ProB.
In Proceedings SEFM'16, LNCS, 9763, Springer, 2016.
- PDF
Lukas Ladenberger, Michael Leuschel
BMotionWeb: A Tool for Rapid Creation of Formal Prototypes.
In Proceedings SEFM'16, LNCS, 9763, Springer, 2016.
Michael Leuschel
Formal Model-Based Constraint Solving and Document Generation.
In SBMF'2016, Lecture Notes in Computer Science, Springer, 2016.
- PDF
Joy Clark, Jens Bendisposto, Stefan Hallerstede, Dominik Hansen, Michael Leuschel
Generating Event-B Specifications from Algorithm Descriptions.
In Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings, Michael J. Butler and Klaus-Dieter Schewe and Atif Mashkoor and Miklós Biró, Lecture Notes in Computer Science, 9675, Springer, 183--197, 2016.
- LINK

2015

Ladenberger, Lukas, Hansen, Dominik, Wiegard, Harald, Bendisposto, Jens, Leuschel, Michael
Validation of the ABZ landing gear system using ProB.
In International Journal on Software Tools for Technology Transfer, Springer Berlin Heidelberg, 1-17, 2015.
- LINK
David Schneider, Michael Leuschel, Tobias Witt
Model-Based Problem Solving for University Timetable Validation and Improvement.
In FM 2015: Formal Methods: 20th International Symposium, Lecture Notes in Computer Science (Book 9109), Springer, 487-495, 2015.
Philipp Körner, David Schneider, Michael Leuschel
Evaluating Interpreter Design in Prolog.
In 18. Kolloquium Programmiersprachen und Grundlagen der Programmierung KPS 2015, Schriftenreihe des Instituts für Computersprachen, Springer, 2015.
- LINK
Sebastian Krings, Jens Bendisposto, Michael Leuschel
From Failure to Proof: The ProB Disprover for B and Event-B.
In Proceedings SEFM'2015, LNCS 9276, Springer, 2015.
- PDF
Sebastian Krings, Michael Leuschel
Inferring Physical Units in Formal Models.
In Software & Systems Modeling, Springer Berlin Heidelberg, 1-23, 2015.
- PDF
Dominik Hansen, Michael Leuschel
Translating B to TLA+ for Validation with TLC.
Technical Report, Institut für Informatik, Heinrich-Heine-Universität Düsseldorf, STUPS/2015/Feb, 2015.
- PDF
- LINK
Lukas Ladenberger, Michael Leuschel
Mastering the Visualization of Larger State Spaces with Projection Diagrams.
Technical Report, Institut für Informatik, Heinrich-Heine-Universität Düsseldorf, STUPS/2015/May, 2015.
- PDF
- LINK
Lukas Ladenberger, Michael Leuschel
Mastering the Visualization of Larger State Spaces with Projection Diagrams.
In Proceedings ICFEM'2015, LNCS 9407, Springer-Verlag, 153--169, 2015.

2014

Michael Leuschel, Germán Vidal
Fast offline partial evaluation of logic programs.
In Information and Computation, 235, 70--97, 2014.
- PDF
- LINK
Lukas Ladenberger, Ivaylo Dobrikov, Michael Leuschel
An Approach for Creating Domain Specific Visualisations of CSP Models.
In HOFM 2014, Dimitra Giannakopoulou and Gwen Salaün, LNCS, 2014.
- PDF
Ivaylo Dobrikov, Michael Leuschel
Optimising the ProB Model Checker for B using Partial Order Reduction.
In SEFM 2014, Dimitra Giannakopoulou and Gwen Salaün, LNCS 8702, 220--234, 2014.
- PDF
Michael Leuschel, Jens Bendisposto, Ivaylo Dobrikov, Sebastian Krings, Daniel Plagge
From Animation to Data Validation: The ProB Constraint Solver 10 Years On.
In Formal Methods Applied to Complex Systems: Implementation of the B Method, Jean-Louis Boulanger, Wiley ISTE, 427--446, 2014.
- LINK
Ivaylo Dobrikov, Michael Leuschel
Optimising the ProB Model Checker for B using Partial Order Reduction.
Technical Report, Institut für Informatik, Heinrich-Heine-Universität Düsseldorf, STUPS/2014/xx, 2014.
- PDF
Sebastian Krings, Jens Bendisposto, Michael Leuschel
Turning Failure into Proof: Evaluating the ProB Disprover.
In Proceedings of the 1st International Workshop about Sets and Tools, 2014.
- PDF
John Witulski, Michael Leuschel
Checking Computations of Formal Method Tools - A Secondary Toolchain for ProB.
In Proceedings of the 1st Workshop on Formal-IDE, EPTCS, 149, Electronic Proceedings in Theoretical Computer Science, 2014.
- PDF
Jens Bendisposto, Sebastian Krings, Michael Leuschel
Who watches the watchers: Validating the ProB Validation Tool.
In Proceedings of the 1st Workshop on Formal-IDE, EPTCS, 149, Electronic Proceedings in Theoretical Computer Science, 2014.
- PDF
Dominik Hansen, Lukas Ladenberger, Harald Wiegard, Jens Bendisposto, Michael Leuschel
Validation of the ABZ Landing Gear System using ProB.
In ABZ 2014: The Landing Gear Case Study, 2014.
- PDF
Dominik Hansen, Jens Bendisposto, Michael Leuschel
Integrating ProB into the TLA Toolbox.
In TLA Workshop, 2014.
- PDF
Dominik Hansen, Michael Leuschel
Translating B to TLA + for Validation with TLC.
In Proceedings ABZ'14, LNCS 8477, 40--55, 2014.
- PDF
Michael Leuschel, David Schneider
Towards B as a High-Level Constraint Modelling Language.
In Abstract State Machines, Alloy, B, TLA, VDM, and Z, Ait Ameur, Yamine and Schewe, Klaus-Dieter, Lecture Notes in Computer Science, 8477, Springer Berlin Heidelberg, 101-116, 2014.
- PDF
- LINK
Michael Leuschel
Towards Constraint-Solving over Higher-Order Unbounded Datatypes using Formal Methods Tools.
In VPT 2014, Alexei Lisitsa and Andrei Nemytykh, EPiC Series, 28, EasyChair, 1-1, 2014.
- LINK

2013

Stefan Hallerstede, Michael Leuschel, Daniel Plagge
Validation of Formal Models by Refinement Animation.
In Science of Computer Programming, 78, 3, 272--292, 2013.
- PDF
Jens Bendisposto, Joy Clark, Ivaylo Dobrikov, Philipp Körner, Sebastian Krings, Lukas Ladenberger, Michael Leuschel, Daniel Plagge
ProB 2.0 Tutorial.
In Proceedings of the 4th Rodin User and Developer Workshop, TUCS Lecture Notes, TUCS, 2013.
- PDF
- LINK
Jens Bendisposto, Philipp Körner, Michael Leuschel
Parallel Model Checking of B Specifications.
In Proceedings of the 4th Rodin User and Developer Workshop, TUCS Lecture Notes, TUCS, 2013.
- PDF
Sebastian Krings, Jens Bendisposto, Ivaylo Dobrikov, Michael Leuschel
B constrained.
In Proceedings of the 4th Rodin User and Developer Workshop, TUCS Lecture Notes, TUCS, 2013.
- PDF
Sebastian Krings, Michael Leuschel
Inferring Physical Units in B Models.
In Proceedings SEFM'2013, LNCS 8137, Springer, 137--151, 2013.
- PDF
Jerome Falampin, Hung Le-Dang, Michael Leuschel, Mikael Mokrani, Daniel Plagge
Improving Railway Data Validation with ProB.
In Industrial Deployment of System Engineering Methods, Springer, 27--44, 2013.
- PDF
- LINK
Dominik Hansen, Michael Leuschel
Translating B to TLA+ for Validation with TLC.
Technical Report, Institut für Informatik, Heinrich-Heine-Universität Düsseldorf, STUPS/2013/xx, 2013.
- PDF
- LINK

2012

Thierry Lecomte, Lilian Burdy, Michael Leuschel
Formally Checking Large Data Sets in the Railways.
In CoRR, abs/1210.6815, 2012.
- PDF
Dominik Hansen, Michael Leuschel
Translating TLA+ to B for Validation with ProB.
In Proceedings iFM'2012, LNCS 7321, Springer, 24--38, 2012.
- PDF
Daniel Plagge, Michael Leuschel
Validating B, Z and TLA+ using ProB and Kodkod.
In Proceedings FM'2012, Dimitra Giannakopoulou and Dominique Méry, LNCS 7436, Springer, 372--386, 2012.
- PDF

2011

Michael Leuschel, Jérôme Falampin, Fabian Fritz, Daniel Plagge
Automated Property Verification for Large Scale B Models with ProB.
In Formal Aspects of Computing, 23, 6, 683--709, 2011.
- PDF
Bendisposto, Jens, Fritz, Fabian, Jastram, Michael, Leuschel, Michael, Weigelt, Ingo
Developing Camille, a text editor for Rodin.
In Software: Practice and Experience, 41, 2, John Wiley & Sons, Ltd., 189--198, 2011.
- LINK
Jens Bendisposto, Michael Leuschel
Automatic Flow Analysis for Event-B.
In Proceedings of Fundamental Approaches to Software Engineering (FASE) 2011, Dimitra Giannakopoulou and Fernando Orejas, Lecture Notes in Computer Science, 6603, Springer, 50--64, 2011.
- PDF
Stefan Hallerstede, Michael Leuschel
Constraint-Based Deadlock Checking of High-Level Specifications.
In Theory and Practice of Logic Programming, 11, 4--5, Cambridge University Press, 767--782, 2011.
- PDF
Stefan Hallerstede, Michael Leuschel
Finding Deadlocks of Event-B Models by Constraint Solving.
In B2011 Workshop (short paper), 2011.
- PDF
Carl Friedrich Bolz, Antonio Cuni, Maciej Fijałkowski, Michael Leuschel, Samuele Pedroni, Armin Rigo
Allocation removal by partial evaluation in a tracing JIT.
In PEPM, 2011.
- PDF
Rainer Gmehlich, Katrin Grau, Stefan Hallerstede, Michael Leuschel, Felix Lösch, Daniel Plagge
On Fitting a Formal Method into Practice.
In Proceedings ICFEM'2011, Shengchao Qin and Zongyan Qiu, Lecture Notes in Computer Science, 6991, Springer, 195--210, 2011.
- PDF
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.
In Proceedings of the 6th workshop on the Implementation, Compilation, Optimization of Object-Oriented Languages and Programming Systems, ICOOOLPS '11, 2011.
- PDF

2010

Michael Leuschel, Salvador Tamarit, Germán Vidal
Fast and Accurate Strong Termination Analysis with an Application to Partial Evaluation.
In Proceedings WFLP'2009, Santiago Escobar, LNCS 5979, Springer-Verlag, 111--127, 2010.
- PDF
Stefan Hallerstede, Michael Leuschel, Daniel Plagge
Refinement-Animation for Event-B - Towards a Method of Validation.
In Proceedings ABZ'2010, Lecture Notes in Computer Science, 5977, Springer-Verlag, 287--301, 2010.
- PDF
Edd Turner, Michael Butler, Michael Leuschel
A Refinement-Based Correctness Proof of Symmetry Reduced Model Checking.
In Proceedings ABZ'2010, Lecture Notes in Computer Science, 5977, Springer-Verlag, 231--244, 2010.
- PDF
Daniel Plagge, Michael Leuschel
Seven at one stroke: LTL model checking for High-level Specifications in B, Z, CSP, and more.
In Software Tools for Technology Transfer (STTT), 12, 1, Springer-Verlag, 9--21, 2010.
- PDF
Michael Leuschel, Thierry Massart
Efficient Approximate Verification of B via Symmetry Markers.
In Annals of Mathematics and Artificial Intelligence, 59, 1, 81--106, 2010.
- PDF
Carl Friedrich Bolz, Michael Leuschel, David Schneider
Towards a Jitting VM for Prolog Execution.
In PPDP '10 - Proceedings of the 12th international ACM SIGPLAN symposium on Principles and practice of declarative programming, ACM, 2010.
- PDF
David Schneider, Carl Friedrich Bolz, Michael Leuschel
Jitting Prolog for Fun and Profit.
In DYLA 2010 - 4th Workshop on Dynamic Languages and Applications, 2010.
- PDF
Michael Leuschel, Jens Bendisposto
Directed Model Checking for B: An Evaluation and New Techniques.
In SBMF'2010, Jim Davies and Leila Silva and Adenilso da Silva Simão, Lecture Notes in Computer Science, 6527, Springer, 1--16, 2010.
- PDF
Jens Bendisposto, Michael Leuschel, Markus Borgermans
GEPAVAS Gerichtete und parallele Validierung von abstrakten Spezifikationen - Projektreport.
Technical Report, University of Düsseldorf, 2010.
- PDF
Michael Jastram, Stefan Hallerstede, Michael Leuschel, Aryldo G Russo Jr
An Approach of Requirements Tracing in Formal Refinement.
In VSTTE, Lecture Notes in Computer Science, 6217, Springer, 97-111, 2010.
- PDF

2009

Michael Leuschel, Dominique Cansell, Michael Butler
Validating and Animating Higher-Order Recursive Functions in B.
In Festschrift for Egon Börger, Jean-Raymond Abrial and Uwe Glässer, Lecture Notes in Computer Science, 5115, Springer-Verlag, 2009.
- PDF
Carl Friedrich Bolz, Michael Leuschel, Armin Rigo
Towards Just-In-Time Partial Evaluation of Prolog.
In Logic-Based Program Synthesis and Transformation, 19th International Symposium, LOPSTR 2009, Coimbra, Portugal, September 2009, Revised Selected Papers, Danny De Schreye, Lecture Notes in Computer Science, 6037, Springer, 158-172, 2009.
- PDF
Michael Leuschel, Marisa Llorens, Javier Olivier, Josep Silva, Salvador Tamarit
SOC: A Slicer for CSP Specifications.
In PEPM 2009, ACM Press, 2009.
Mireille Samia, Michael Leuschel
Pie Tree Visualization.
In Proceedings SEKE, Knowledge Systems Institute, 400--405, 2009.
Michael Leuschel, Jérôme Falampin, Fabian Fritz, Daniel Plagge
Automated Property Verification for Large Scale B Models.
In Proceedings FM 2009, Lecture Notes in Computer Science, 5850, Springer-Verlag, 708--723, 2009.
- PDF
Daniel Plagge, Michael Leuschel, Ilya Lopatkin, Alexander Romanovsky
SAL, Kodkod, and BDDs for Validation of B Models. Lessons and Outlook.
In Proceedings AFM 2009, 16--22, 2009.
- PDF
Jens Bendisposto, Michael Leuschel
Proof Assisted Model Checking for B.
In Proceedings of ICFEM 2009, Karin Breitman and Ana Cavalcanti, Lecture Notes in Computer Science, 5885, Springer, 504-520, 2009.
- PDF
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.
In Proceedings TESTCOM/FATES 2009, Lecture Notes in Computer Science, 5826, Springer-Verlag, 179--194, 2009.
- PDF
Lukas Ladenberger, Jens Bendisposto, Michael Leuschel
Visualising Event-B Models with B-Motion Studio.
In Proceedings of FMICS 2009, Marı́a Alpuente and Byron Cook and Christophe Joubert, Lecture Notes in Computer Science, 5825, Springer, 202-204, 2009.
- PDF
Stefan Hallerstede, Michael Leuschel
How to explain mistakes.
In TFM 2009, Lecture Notes in Computer Science, Springer-Verlag, 105--124, 2009.
- PDF
Mireille Samia, Harald Wiegard, Jens Bendisposto, Michael Leuschel
High-Level versus Low-Level Specifications: Comparing B with Promela and ProB with Spin.
In Proceedings TFM-B 2009, Attiogbe and Mery, APCB, 2009.
- PDF
Jens Bendisposto, Michael Leuschel
Parallel Model Checking of Event-B Specification with ProB.
In 2009.

2008

Michael Leuschel, Michael Butler
ProB: An Automated Analysis Toolset for the B Method.
In Software Tools for Technology Transfer (STTT), 10, 2, Springer-Verlag, 185--203, 2008.
- PDF
Michael Leuschel, Mireille Samia, Jens Bendisposto, Li Luo
Easy Graphical Animation and Formula Viewing for Teaching B.
In The B Method: from Research to Teaching, C. Attiogbé and H. Habrias, Lina, 17--32, 2008.
- PDF
Corinna Spermann, Michael Leuschel
ProB gets Nauty: Effective Symmetry Reduction for B and Z Models.
In Proceedings TASE 2008, IEEE, 15--22, 2008.
- PDF
Michael Leuschel
The High Road to Formal Validation: Model Checking High-Level versus Low-Level Specifications.
In ABZ 2008, Lecture Notes in Computer Science, 5238, Springer-Verlag, 4--23, 2008.
- PDF
Michael Leuschel
Declarative Programming for Verification: Lessons and Outlook.
In Proceedings PPDP'2008, ACM Press, 1--7, 2008.
- PDF
Michael Leuschel, Germán Vidal
Fast Offline Partial Evaluation for Large Logic Programs.
In Proceedings LOPSTR'08, Michael Hanus, Lecture Notes in Computer Science, 5438, 119--134, 2008.
- PDF
Michael Leuschel, Marisa Llorens, Javier Olivier, Josep Silva, Salvador Tamarit
Static Slicing of CSP Specifications.
In Preproceedings LOPSTR'08, Michael Hanus, Lecture Notes in Computer Science, 5438, 103--118, 2008.
- PDF
Michael Leuschel, Marc Fontaine
Probing the Depths of CSP-M: A new FDR-compliant Validation Tool.
In ICFEM 2008, Springer-Verlag, 278--297, 2008.
- PDF
Jens Bendisposto, Ian Endrijautzki, Michael Leuschel, David Schneider
A Semantics-Aware Editing Environment for Prolog in Eclipse.
In Proceedings of the 18th Workshop on Logic-based methods in Programming Environments, WLPE, 2008.
- PDF
Jens Bendisposto, Michael Leuschel, O. Ligot, Mireille Samia
La validation de modèles Event-B avec le plug-in ProB pour RODIN.
In Technique et Science Informatiques, 27, 8, 1065-1084, 2008.
Steve Barker, Michael Leuschel, Mauricio Varea
Efficient and Flexible Access Control via Jones-Optimal Logic Program Specialisation.
In Higher-Order and Symbolic Computation, 21, 1--2, 5--35, 2008.
- PDF

2007

Dragan Bosnacki, Alastair F. Donaldson, Michael Leuschel, Thierry Massart
Efficient Approximate Verification of Promela Models via Symmetry Markers.
In ATVA, Lecture Notes in Computer Science, 4762, Springer-Verlag, 300--315, 2007.
- PDF
Jens Bendisposto, Michael Leuschel
BE4: The B Extensible Eclipse Editing Environment.
In Proceedings of B 2007, Jacques Julliand and Olga Kouchnarenko, Lecture Notes in Computer Science, 4355, Springer, 270-273, 2007.
- PDF
Karl Klose, Klaus Ostermann, Michael Leuschel
Partial Evaluation of Pointcuts.
In Practical Applications of Declarative Languages (PADL'07), Lecture Notes in Computer Science, Springer-Verlag, 320--334, 2007.
- PDF
Jens Bendisposto, Michael Leuschel
A Generic Flash-Based Animation Engine for ProB.
In Proceedings of B 2007, Jacques Julliand and Olga Kouchnarenko, Lecture Notes in Computer Science, 4355, Springer, 266-269, 2007.
- PDF
Michael Leuschel, Michael Butler, Corinna Spermann, Edd Turner
Symmetry Reduction for B by Permutation Flooding.
In Proceedings B'2007, Lecture Notes in Computer Science, 4355, Springer-Verlag, 79--93, 2007.
- PDF
Michael Leuschel, Thierry Massart
Efficient Approximate Verification of B via Symmetry Markers.
In Proceedings International Symmetry Conference, 71--85, 2007.
- PDF
Manoranjan Satpathy, Michael Butler, Michael Leuschel, S. Ramesh
Automatic Testing from Formal Specifications.
In Tests and Proofs (TAP 2007), Lecture Notes in Computer Science, 4454, Springer-Verlag, 95--113, 2007.
Edd Turner, Michael Leuschel, Corinna Spermann, Michael Butler
Symmetry Reduced Model Checking for B.
In Proceedings TASE 2007, IEEE, 25--34, 2007.
- PDF
Daniel Plagge, Michael Leuschel
Validating Z Specifications using the ProB Animator and Model Checker.
In Integrated Formal Methods, J. Davies and J. Gibbons, Lecture Notes in Computer Science, 4591, Springer-Verlag, 480--500, 2007.
- PDF
Olivier Ligot, Jens Bendisposto, Michael Leuschel
Debugging Event-B Models using the ProB Disprover Plug-in.
In Proceedings AFADL'07, 2007.
- PDF
Michael Leuschel, Daniel Plagge
Seven at one stroke: LTL model checking for High-level Specifications in B, Z, CSP, and more.
Technical Report, Institut für Informatik, Heinrich-Heine-Universität Düsseldorf, STUPS/2007/02, 2007.
- PDF
Michael Leuschel, Daniel Plagge
Seven at one stroke: LTL model checking for High-level Specifications in B, Z, CSP, and more.
In ISoLA, Yamine Aı̈t Ameur and Frédéric Boniol and Virginie Wiels, Revue des Nouvelles Technologies de l'Information, RNTI-SM-1, Cépaduès-Éditions, 73--84, 2007.

2006

Michael Leuschel, Daniel Elphick, Mauricio Varea, Stephen Craig, Marc Fontaine
The Ecce and Logen Partial Evaluators and their Web Interfaces.
In Proceedings PEPM 06, John Hatcliff and Frank Tip, IBM Press, 88--94, 2006.
- PDF
Michael Leuschel, Stephen Craig, Daniel Elphick
Supervising Offline Partial Evaluation of Logic Programs using Online Techniques.
In Proceedings LOPSTR'06, German Puebla, Lecture Notes in Computer Science, 4407, Springer-Verlag, 43--59, 2006.
- PDF
Stephane Lo Presti, Michael Butler, Michael Leuschel, Chris Booth
Holistic Trust Design of E-Services.
In Trust in E-services: Technologies, Practices and Challenges, Ronggong Song and Larry Korba and George Yee, IGI Global, 113--139, 2006.
Michael Leuschel, Jens Bendisposto
Animating and Model Checking B Specifications with Higher-Order Recursive Functions.
In Dagstuhl Seminar 06191 "Rigorous Methods for Software Construction and Analysis", J. Abrial, U. Glässer, 2006.
- PDF

2005

Michael Leuschel, Michael Butler
Combining CSP and B for Specification and Property Verification.
In FM'2005, John Fitzgerald and Ian Hayes and Andrzej Tarlecki, Lecture Notes in Computer Science, 3582, Springer-Verlag, 221--236, 2005.
- PDF
Michael Butler, Michael Leuschel, Colin Snook
Tools for system validation with B abstract machines.
In 12th International Workshop on Abstract State Machines, 57--69, 2005.
- PDF
Michael Leuschel
Guest Editorial -- Special Issue on Automated Verification of Critical Systems.
In Formal Aspects of Computing, 17, 2, Springer-Verlag, 91-92, 2005.
Michael Leuschel, Michael Butler
Automatic Refinement Checking for B.
In Proceedings ICFEM, Kung-Kiu Lau and Richard Banach, Lecture Notes in Computer Science, 3785, Springer-Verlag, 345--359, 2005.
- PDF
Michael Leuschel, Stephen Craig
A Reconstruction of the Lloyd-Topor Transformation using Partial Evaluation.
In Pre-Proceedings of LOPSTR'05, Pat Hill, 2005.
- PDF
Michael Leuschel, Edd Turner
Visualising Larger State Spaces in ProB.
In ZB, Helen Treharne and Steve King and Martin Henson and Steve Schneider, Lecture Notes in Computer Science, 3455, Springer-Verlag, 6--23, 2005.
- PDF
Michael Leuschel, Germán Vidal
Forward Slicing by Conjunctive Partial Deduction and Argument Filtering.
In ESOP, Mooly Sagiv, Lecture Notes in Computer Science, 3444, Springer-Verlag, 61--76, 2005.
- PDF
Stephane Lo Presti, Michael Butler, Michael Leuschel, Chris Booth
A Trust Analysis Methodology for Pervasive Computing Systems.
In Trusting Agents for trusting Electronic Societies, R Falcone and S Barber and J Sabater and M Singh, Lecture Notes in Computer Science, 3577, Springer-Verlag, 2005.
- PDF
Manoranjan Satpathy, Michael Leuschel, Michael Butler
ProTest: An Automatic Test Environment for B Specifications.
In Electronic Notes in Theroretical Computer Science, 111, Elsevier, 113--136, 2005.
- PDF
Qian Wang, Gopal Gupta, Michael Leuschel
Towards Provably Correct Code Generation via Horn Logical Continuation Semantics.
In PADL, Manuel Hermengildo and Daniel Cabeza, Lecture Notes in Computer Science, 3350, Springer-Verlag, 98--112, 2005.
- PDF
Stephen Craig, Michael Leuschel
Self-Tuning Resource Aware Specialisation for Prolog.
In Proceedings PPDP'2005, ACM Press, 23--34, 2005.
- PDF

2004

Steve Barker, Michael Leuschel, Mauricio Varea
Efficient and Flexible Access Control via Logic Program Specialisation.
In PEPM, Nevin Heintze and Peter Sestoft, ACM Press, 190--119, 2004.
- PDF
Michael Butler, Michael Leuschel, Stephane Lo Presti, Phillip Turner
The Use of Formal Methods in the Analysis of Trust (Position Paper).
In iTrust, Christian Jensen and Stefan Poslad and Theo Dimitrakos, Lecture Notes in Computer Science, 2995, Springer-Verlag, 333--339, 2004.
Stephen Craig, John Gallagher, Michael Leuschel, Kim S. Henriksen
Fully Automatic Binding Time Analysis for Prolog.
In LOPSTR, Sandro Etalle, Lecture Notes in Computer Science, 3573, Springer-Verlag, 53--68, 2004.
- PDF
Stephen Craig, Michael Leuschel
Lix: An Effective Self-applicable Partial Evaluator for Prolog.
In FLOPS, Yukiyoshi Kameyama and Peter J. Stuckey, Springer-Verlag, 85--99, 2004.
- PDF
Michael Leuschel
A Framework for the Integration of Partial Evaluation and Abstract Interpretation of Logic Programs.
In ACM Transactions on Programming Languages and Systems (TOPLAS), 26, 3, ACM, 413--463, 2004.
- PDF
Michael Leuschel
ProB: Un outil de modélisation formelle (Invited Talk).
In JFPLC, Fred Mesnard, Hermes Science Publications, Lavoisier, 13--13, 2004.
- PDF
Michael Leuschel, Stephen Craig, Maurice Bruynooghe, Wim Vanhoof
Specializing Interpreters using Offline Partial Deduction.
In Program Development in Computational Logic, Maurice Bruynooghe and Kung-Kiu Lau, Lecture Notes in Computer Science, 3049, Springer-Verlag, 341--376, 2004.
- PDF
Michael Leuschel, Jesper Jørgensen, Wim Vanhoof, Maurice Bruynooghe
Offline Specialisation in Prolog Using a Hand-Written Compiler Generator.
In TPLP, 4, 1--2, Cambridge University Press, 139--191, 2004.
- PDF
Michael Leuschel, Edd Turner
Visualising Larger State Spaces in ProB.
Technical Report, ECS, University of Southampton, 2004.
Stephane Lo Presti, Michael Butler, Michael Leuschel, Colin Snook, Phillip Turner
Formal Modelling and Verification of Trust in a Pervasive Application.
Technical Report, DSSE, University of Southampton, 2004.
- PDF
Wim Vanhoof, Maurice Bruynooghe, Michael Leuschel
Binding-Time Analysis for Mercury.
In Program Development in Computational Logic, Maurice Bruynooghe and Kung-Kiu Lau, Lecture Notes in Computer Science, 3049, Springer-Verlag, 189--232, 2004.
- PDF
Berndt Farwer, Michael Leuschel
Model Checking of Object Petri Nets in Prolog.
In PPDP, Eugenio Moggi and David Scott Warren, ACM Press, 20--31, 2004.
- PDF

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.
In ER (Workshops), Manfred A. Jeusfeld and Oscar Pastor, Lecture Notes in Computer Science, 2814, Springer Verlag, 17--28, 2003.
- PDF
Juan Carlos Augusto, Michael Leuschel, Michael Butler, Carla Ferreira
Using the Extensible Model Checker XTL to Verify StAC Business Specifications.
In AVoCS, Michael Leuschel and Stefan Gruner and Stephane Lo Presti, 253--266, 2003.
- PDF
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.
In IEEE Computing, 2, 3, 96, 2003.
- PDF
Stephen Craig, Michael Leuschel
A Compiler Generator for Constraint Logic Programs.
In Ershov Memorial Conference, M. Broy and A. Zamulin, Lecture Notes in Computer Science, 2890, Springer-Verlag, 2003.
- PDF
Daniel Elphick, Michael Leuschel, Simon J. Cox
Partial Evaluation of MATLAB.
In Generative Programming and Component Engineering, Second International Conference, GPCE 2003, Erfurt, Germany, September 22-25, 2003, Proceedings, 344--363, 2003.
- LINK
Helko Lehmann, Michael Leuschel
Inductive Theorem Proving by Program Specialisation: Generating proofs for Isabelle using Ecce (Invited talk).
In LOPSTR, Maurice Bruynooghe, Lecture Notes in Computer Science, 3018, Springer-Verlag, 1--19, 2003.
- PDF
Michael Leuschel, Michael Butler
ProB: A Model Checker for B.
In FME, Araki Keijiro and Stefania Gnesi and Mandrio Dino, Lecture Notes in Computer Science, 2805, Springer-Verlag, 855--874, 2003.
- PDF
Michael Leuschel, Stephen Craig, Maurice Bruynooghe, Wim Vanhoof
Specializing Interpreters using Offline Partial Deduction.
Technical Report, ECS, University of Southampton, DSSE-TR-2003-5, 2003.
- PDF
Mauricio Varea, Michael Leuschel, Bashir Al-Hashimi
Improving Compositional Verification of State-based Models by Reducing Modular Unbalance.
In Refinement of Critical Systems, 2003.
- PDF

2002

Helko Lehmann, Michael Leuschel
Generating inductive verification proofs for Isabelle using the partial evaluator Ecce.
Technical Report, ECS, University of Southampton, DSSE-TR-2002-02, 2002.
Michael Leuschel
Homeomorphic Embedding for Online Termination of Symbolic Methods.
In The Essence of Computation -- Essays dedicated to Neil Jones, Torben Mogensen, David Schmidt, I. H. Sudborough, Lecture Notes in Computer Science, 2566, Springer-Verlag, 379--403, 2002.
- PDF
Michael Leuschel, Maurice Bruynooghe
Logic program specialisation through partial deduction: Control Issues.
In Theory and Practice of Logic Programming, 2, 4--5, Cambridge University Press, 461--515, 2002.
- PDF
Michael Leuschel, Stefan Gruner
Abstract Conjunctive Partial Deduction using Regular Types and its Application to Model Checking.
In LOPSTR, Alberto Pettorossi, Lecture Notes in Computer Science, 2372, Springer-Verlag, 91--110, 2002.
Michael Leuschel, Thierry Massart
Logic programming and partial deduction for the verification of reactive systems: An experimental evaluation.
In AVoCS, Gethin Norman and Martha Kwiatkowska and Dimitar Guelev, University of Birmingham, 143--149, 2002.
- PDF
Mauricio Varea, Bashir Al-Hashimi, Michael Leuschel
Finite and Infinite Model Checking of Dual Transition Petri Net Models.
In AVoCS, 265--269, 2002.
- PDF

2001

Laksono Adhianto, Michael Leuschel
Strategy for Improving Memory Locality Reuse and Exploiting Hidden Parallelism.
In Proceedings of ISSM, 2001.
Hugh Glaser, Pieter H. Hartel, Michael Leuschel, Andrew Martin
Declarative Languages in Education.
In Encyclopaedia of Microcomputers, 27, Marcel Dekker Inc, 79--102, 2001.
- PDF
Michael Leuschel
Design and Implementation of the High-Level Specification Language CSP(LP).
In PADL, Lecture Notes in Computer Science, 1990, Springer, 14--28, 2001.
- PDF
Michael Leuschel, Laksono Adhianto, Michael Butler, Carla Ferreira, Leonid Mikhailov
Animation and Model Checking of CSP and B using Prolog Technology.
In Proceedings of the ACM Sigplan Workshop on Verification and Computational Logic, Michael Leuschel and Andreas Podelski and C.R. Ramakrishnan and Ulrich Ultes-Nitsche, 97--109, 2001.
Michael Leuschel, Thierry Massart, Andrew Currie
How to make FDR Spin: LTL model checking of CSP using Refinement.
In Proceedings FME'2001, J.N. Oliviera, P. Zave, Springer-Verlag, 99--118, 2001.
- PDF
Michael Leuschel, Ivan Wolton, Thierry Massart, Laksono Adhianto
Temporal Logic Model Checking of CSP: Tools and Techniques.
In AVoCS 2001, David Nowak, Oxford University Computing Laboratory, 2001.

2000

Andrew Currie, Michael Leuschel, Thierry Massart
LTL Model Checking of CSP by Refinement: How to Make FDR Spin.
In Proceedings VCL'2000, 2000.
Helko Lehmann, Michael Leuschel
Decidability Results for the Propositional Fluent Calculus.
In Computational Logic, John LLoyd, Lecture Notes in Computer Science, 1861, Springer-Verlag, 762--776, 2000.
Helko Lehmann, Michael Leuschel
Solving Planning Problems by Partial Deduction.
In LPAR, Michel Parigot and Andrei Voronkov, Lecture Notes in Computer Science, 1955, Springer-Verlag, 2000.
- PDF
Michael Leuschel, Maurice Bruynooghe
Control Issues in Partial Deduction: The Ever Ending Story.
Technical Report, University of Southampton, 2000.
Michael Leuschel, Helko Lehmann
Coverability of Reset Petri Nets and other Well-Structured Transition Systems by Partial Deduction.
In Computational Logic, John Lloyd and Verónica Dahl and Ulrich Furbach and Manfred Kerber and Kung-Kiu Lau and Catuscia Palamidessi and Luı́s Moniz Pereira and Yehoshua Sagiv and Peter J. Stuckey, Lecture Notes in Computer Science, 1861, Springer-Verlag, 101--115, 2000.
- PDF
Michael Leuschel, Helko Lehmann
Solving Coverability Problems of Petri Nets by Partial Deduction.
In PPDP, Maurizio Gabbrielli and Frank Pfenning, ACM Press, 268--279, 2000.
- PDF

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.
In Journal of Logic Programming, 41, 2--3, 231--277, 1999.
- PDF
Robert Glueck, Michael Leuschel
Abstraction-Based Partial Deduction for Solving Inverse Problems -- A Transformational Approach to Software Verification.
In Ershov Memorial Conference, Lecture Notes in Computer Science, 1755, Springer-Verlag, 93--100, 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.
In Proc. 4th Int. Workshop on Formal Methods for Industrial Critical Systems, S. Gnesi and D. Latella, STAR/CNR, Pisa, Italy, 179--203, 1999.
Michael Leuschel
Advanced Logic Program Specialisation.
In Partial Evaluation - Practice and Theory, DIKU 1998 International Summer School, Springer-Verlag, 271--292, 1999.
- PDF
Michael Leuschel
Logic Program Specialisation.
In Partial Evaluation: Practice and Theory, John Hatcliff and Torben AE Mogensen and Peter Thiemann, Lecture Notes in Computer Science, 1706, Springer-Verlag, 155--188, 1999.
- PDF
Michael Leuschel, Jesper Jørgensen
Efficient Specialisation in Prolog Using the Hand-Written Compiler Generator LOGEN.
In Electronic Notes in Theoretical Computer Science, 30, 2, 157-162, 1999.
Michael Leuschel, Jesper Jørgensen
Efficient Specialisation in Prolog Using a Hand-Written Compiler Generator.
Technical Report, University of Southampton, DSSE-TR-99-6, 1999.
Michael Leuschel, Nick Linnenbruegger, Jerome Thoma
Analyzing Context-Free and Context-Sensitive Grammars by Abstract Interpretation.
In Proceedings of the Formal Grammar Conference FG'99, G-J. M. Kruijff and R. T. Oerle, University of Utrecht, 93--101, 1999.
Michael Leuschel, Thierry Massart
Infinite State Model Checking by Abstract Interpretation and Program Specialisation.
In LOPSTR '99, A. Bossi, Lecture Notes in Computer Science, 1817, Springer-Verlag, 63--82, 1999.
- PDF
Jonathan C. Martin, Michael Leuschel
Sonic Partial Deduction.
In Ershov Memorial Conference, Lecture Notes in Computer Science, 1755, Springer-Verlag, 101--112, 1999.

1998

Maurice Bruynooghe, Michael Leuschel, Konstantinos Sagonas
A Polyvariant Binding-Time Analysis for Off-line Partial Deduction.
In ESOP, C. Hankin, Lecture Notes in Computer Science, 1381, Springer-Verlag, 27--41, 1998.
- PDF
Stefaan Decorte, Danny De Schreye, Michael Leuschel, Bern Martens, Konstantinos Sagonas
Termination Analysis for Tabled Logic Programming.
In LOPSTR '97, N. Fuchs, Lecture Notes in Computer Science, 1463, Springer-Verlag, 111--127, 1998.
- PDF
Michael Leuschel
Improving Homeomorphic Embedding for Online Termination.
In LOPSTR '98, P. Flener, Lecture Notes in Computer Science, 1559, Springer-Verlag, 199--218, 1998.
- PDF
Michael Leuschel
On the Power of Homeomorphic Embedding for Online Termination.
In Proceedings SAS, Giorgio Levi, Lecture Notes in Computer Science, 1503, Springer-Verlag, 230--245, 1998.
- PDF
Michael Leuschel
Program Specialisation and Abstract Interpretation Reconciled.
In IJCSLP, J. Jaffar, MIT Press, 220--234, 1998.
- PDF
Michael Leuschel, Danny De Schreye
Constrained Partial Deduction and the Preservation of Characteristic Trees.
In New Generation Computing, 16, 3, 283--342, 1998.
Michael Leuschel, Danny De Schreye
Creating Specialised Integrity Checks Through Partial Evaluation of Meta-interpreters.
In Journal of Logic Programming, 36, 2, 149--193, 1998.
- PDF
Michael Leuschel, Bern Martens, Danny De Schreye
Controlling Generalisation and Polyvariance in Partial Deduction of Normal Logic Programs.
In ACM Transactions on Programming Languages and Systems, 20, 1, 208--258, 1998.
Michael Leuschel, Bern Martens, Danny De Schreye
Some Achievements and Prospects in Partial Deduction.
In ACM Computing Surveys, 30, 3es, 1998.
Michael Leuschel, Bern Martens, Konstantinos Sagonas
Preserving Termination of Tabled Logic Programs While Unfolding.
In LOPSTR '97, N. Fuchs, Lecture Notes in Computer Science, 1463, Springer-Verlag, 189--205, 1998.
- PDF
Konstantinos Sagonas, Michael Leuschel
Extending Partial Deduction to Tabled Execution: Some Results and Open Issues.
In ACM Computing Surveys, 30, 3es, 1998.

1997

Michael Leuschel
Advanced Techniques for Logic Program Specialisation.
In AI Communications, 10, 2, 127--128, 1997.
Michael Leuschel
Specialization of Declarative Programs and its Application (workshop overview).
In ILPS, MIT Press, 413--414, 1997.
Michael Leuschel
The Ecce Partial Deduction System.
In Proceedings of the ILPS'97 Workshop on Tools and Environments for (Constraint) Logic Programming, German Puebla, Universidad Politécnica de Madrid Tech. Rep. CLIP7/97.1, 1997.
Michael Leuschel
Advanced Techniques for Logic Program Specialisation.
PhD Thesis, K.U. Leuven, 1997.
- PDF

1996

Jesper Jørgensen, Michael Leuschel
Efficiently Generating Efficient Generating Extensions in Prolog.
In Dagstuhl Seminar on Partial Evaluation, O. Danvy and R. Glueck and P. Thiemann, Lecture Notes in Computer Science, 1110, Springer-Verlag, 238--262, 1996.
- PDF
Jesper Jørgensen, Michael Leuschel, Bern Martens
Conjunctive Partial Deduction in Practice.
In LOPSTR, J. Gallagher, Lecture Notes in Computer Science, 1207, Springer-Verlag, 59--82, 1996.
- PDF
Michael Leuschel
Specialised Integrity Checking by Combining Conjunctive Partial Deduction and Abstract Interpretation.
In Proc. Logic Databases and the Meaning of Change: Dagstuhl-Seminar-Report 157, J. Bocca and H. Decker and A. Voronkov, IBFI GmbH, Schloss Dagstuhl, 18--19, 1996.
Michael Leuschel, Danny De Schreye
Logic Program Specialisation: How To Be More Specific.
In Proceedings PLILP'96, H. Kuchen and S. D. Swierstra, Lecture Notes in Computer Science, 1140, Springer-Verlag, 137--151, 1996.
- PDF
Michael Leuschel, Danny De Schreye
Logic Program Specialisation: How To Be More Specific (abstract).
In LOPSTR, J. Gallagher, Lecture Notes in Computer Science, 1207, Springer-Verlag, 58, 1996.
Michael Leuschel, Danny De Schreye, D. Andre de Waal
A Conceptual Embedding of Folding into Partial Deduction: Towards a Maximal Integration.
In JICSLP, M. Maher, MIT Press, 319--332, 1996.
- PDF
Michael Leuschel, Bern Martens
Global Control for Partial Deduction through Characteristic Atoms and Global Trees.
In Dagstuhl Seminar on Partial Evaluation, O. Danvy and R. Glueck and P. Thiemann, Lecture Notes in Computer Science, 1110, Springer-Verlag, 263--283, 1996.
- PDF
Michael Leuschel, Morten Heine Sørensen
Redundant Argument Filtering of Logic Programs.
In LOPSTR, J. Gallagher, Lecture Notes in Computer Science, 1207, Springer-Verlag, 83--103, 1996.

1995

Michael Leuschel, Danny De Schreye
Towards Creating Specialised Integrity Checks Through Partial Evaluation of Meta-Interpreters.
In PEPM, ACM Press, 253--263, 1995.
- PDF
Michael Leuschel, Danny De Schreye, Bern Martens
Tutorial on Program Specialisation (abstract).
In ILPS, MIT Press, 615--616, 1995.
Michael Leuschel, Bern Martens
Obtaining Specialised Update Procedures through Partial Deduction of the Ground Representation.
In Proc. Joint Workshop on Deductive Databases and Logic Programming and Abduction in Deductive Databases and Knowledge Based Systems, GMD-Studien Nr. 266, 81--95, 1995.
Michael Leuschel, Bern Martens
Partial Deduction of the Ground Representation and its Application to Integrity Checking.
In ILPS, MIT Press, 495--509, 1995.

1994

Michael Leuschel
Partial Evaluation of the "Real Thing".
In LOPSTR, Lecture Notes in Computer Science, 883, Springer-Verlag, 122--137, 1994.

ToC

2025

2024

2023

2022

2021

2020

2019

2018

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

2003

2002

2001

2000

1999

1998

1997

1996

1995

1994