Michael Leuschel

261 papers A 3B 32C 75Misc 5Journal 70Unranked 68
YearRankTypeTitle / Venue / Authors
2026 J jnl
Development and Validation of a Formal Model and Prototype for an Air Traffic Control System.
Formal Aspects Comput.
David Geleßus, Sebastian Stock, Fabian Vu, Michael Leuschel, Atif Mashkoor
2026 C ed.
Rigorous State-Based Methods - 11th International Conference, ABZ 2025, Düsseldorf, Germany, June 10-13, 2025, Proceedings
ABZ
Michael Leuschel, Fuyuki Ishikawa
2026 C conf
Using Prolog to Translate Set Theory and B to SAT.
PADL
Michael Leuschel
2025 — conf
Automated Semantic Validation of Railway Signaling Data on the Basis of Schematron.
RSSRail
Susanne Wunsch, Birgit Jaekel, Martin Lehnert, Christoph Klaus, Jan Gruteser, Michael Leuschel
2025 C conf
Case Study: Safety Controller for Autonomous Driving on Highways.
ABZ
Michael Leuschel, Fabian Vu, Kristin Rutenkolk
2025 J jnl
Certified control for train sign classification.
Sci. Comput. Program.
Jan Roßbach, Michael Leuschel
2025 Misc conf
Failure Divergence Refinement for Event-B.
TASE
Sebastian Stock, Michael Leuschel, Atif Mashkoor
2025 J jnl
Failure divergence refinement for Event-B.
CoRR
Sebastian Stock, Michael Leuschel, Atif Mashkoor
2025 J jnl
Formal Methods in Industry.
Formal Aspects Comput.
Maurice H. ter Beek, Rod Chapman, Rance Cleaveland, Hubert Garavel, Rong Gu, Ivo ter Horst, Jeroen J. A. Keiren, Thierry Lecomte, Michael Leuschel, Kristin Yvonne Rozier, Augusto Sampaio, Cristina Seceleanu, Martyn Thomas, Tim A. C. Willemse, Lijun Zhang
2025 J jnl
Internal and External Performance Fuzzing of Well-Defined Constraints for the B Method.
Formal Aspects Comput.
Jannik Dunkelau, Michael Leuschel
2025 C conf
Promise-Driven Modeling: A Structured Approach for Modeling Cyber-Physical Systems.
FMICS
Felix Schaber, Atif Mashkoor, Michael Leuschel
2024 — conf
B2SAT: A Bare-Metal Reduction of B to SAT.
FM (2)
Michael Leuschel
2024 Misc conf
Evaluating AI-Based Components in Autonomous Railway Systems - A Methodology.
KI
Jan Roßbach, Oliver De Candido, Ahmed Hammam, Michael Leuschel
2024 J jnl
Generating interactive documents for domain-specific validation of formal models.
Int. J. Softw. Tools Technol. Transf.
Fabian Vu, Christopher Happe, Michael Leuschel
2024 C ed.
Rigorous State-Based Methods - 10th International Conference, ABZ 2024, Bergamo, Italy, June 25-28, 2024, Proceedings
ABZ
Silvia Bonfanti, Angelo Gargantini, Michael Leuschel, Elvinia Riccobene, Patrizia Scandurra
2024 — ch.
Specifications are Preferably Amenable to Proof and Animation.
The Practice of Formal Methods (I)
Michael Leuschel
2024 — conf
Towards a Novel Approach to Railway Safety Using STPA and Promise Theory.
SFPVV
Felix Schaber, Atif Mashkoor, Michael Leuschel
2024 J jnl
Trace preservation in B and Event-B refinements.
J. Log. Algebraic Methods Program.
Sebastian Stock, Atif Mashkoor, Michael Leuschel, Alexander Egyed
2024 — conf
Using Formal Models, Safety Shields and Certified Control to Validate AI-Based Train Systems.
FMAS@iFM
Jan Gruteser, Jan Roßbach, Fabian Vu, Michael Leuschel
2024 B conf
Validation of RailML Using ProB.
ICECCS
Jan Gruteser, Michael Leuschel
2024 — conf
Validation of Reinforcement Learning Agents and Safety Shields with ProB.
NFM
Fabian Vu, Jannik Dunkelau, Michael Leuschel
2023 — conf
A Formal Model of Train Control with AI-Based Obstacle Detection.
RSSRail
Jan Gruteser, David Geleßus, Michael Leuschel, Jan Roßbach, Fabian Vu
2023 — conf
Certified Control for Train Sign Classification.
FMAS@iFM
Jan Roßbach, Michael Leuschel
2023 C conf
Modeling and Analysis of a Safety-Critical Interactive System Through Validation Obligations.
ABZ
David Geleßus, Sebastian Stock, Fabian Vu, Michael Leuschel, Atif Mashkoor
2023 C conf
Modeling and Verifying an Arrival Manager Using Event-B.
ABZ
Amel Mammar, Michael Leuschel
2023 — conf
Modelling, Visualisation and Proof of an ETCS Level 3 Moving Block System.
RSSRail
Michael Leuschel, Nader Nayeri
2023 B conf
Performance Fuzzing with Reinforcement-Learning and Well-Defined Constraints for the B Method.
iFM
Jannik Dunkelau, Michael Leuschel
2023 — ch.
ProB: Harnessing the Power of Prolog to Bring Formal Models and Mathematics to Life.
Prolog: The Next 50 Years
Michael Leuschel
2023 C conf
Validation by Abstraction and Refinement.
ABZ
Sebastian Stock, Fabian Vu, David Geleßus, Michael Leuschel, Atif Mashkoor, Alexander Egyed
2023 C conf
Validation of Formal Models by Interactive Simulation.
ABZ
Fabian Vu, Michael Leuschel
2022 J jnl
50 Years of Prolog and Beyond.
CoRR
Philipp Körner, Michael Leuschel, João Barbosa, Vítor Santos Costa, Verónica Dahl, Manuel V. Hermenegildo, José F. Morales, Jan Wielemaker, Daniel Diaz, Salvador Abreu, Giovanni Ciatto
2022 J jnl
Fifty Years of Prolog and Beyond.
Theory Pract. Log. Program.
Philipp Körner, Michael Leuschel, João Barbosa, Vítor Santos Costa, Verónica Dahl, Manuel V. Hermenegildo, José F. Morales, Jan Wielemaker, Daniel Diaz, Salvador Abreu
2022 J jnl
Formalization of Advanced VOs semantics and VO Refinement.
CoRR
Sebastian Stock, Fabian Vu, David Geleßus, Atif Mashkoor, Michael Leuschel, Alexander Egyed
2022 C conf
Generating Domain-Specific Interactive Validation Documents.
FMICS
Fabian Vu, Christopher Happe, Michael Leuschel
2022 J jnl
IVOIRE Deliverable 1.1: Classification of existing VOs & tools and Formalization of VOs semantics.
CoRR
Sebastian Stock, Fabian Vu, Atif Mashkoor, Michael Leuschel, Alexander Egyed
2022 J jnl
Making ProB Compatible with SWI-Prolog.
Theory Pract. Log. Program.
David Geleßus, Michael Leuschel
2022 J jnl
Making ProB compatible with SWI-Prolog.
CoRR
David Geleßus, Michael Leuschel
2022 C conf
Model Checking B Models via High-Level Code Generation.
ICFEM
Fabian Vu, Dominik Brandt, Michael Leuschel
2022 B conf
Operation Caching and State Compression for Model Checking of High-Level Models - How to Have Your Cake and Eat It.
IFM
Michael Leuschel
2022 J jnl
SMT solving for the validation of B and Event-B models.
Int. J. Softw. Tools Technol. Transf.
Joshua Schmidt, Michael Leuschel
2022 — conf
Towards Practical Partial Order Reduction for High-Level Formalisms.
VSTTE
Philipp Körner, Michael Leuschel
2022 C conf
Trace Refinement in B and Event-B.
ICFEM
Sebastian Stock, Atif Mashkoor, Michael Leuschel, Alexander Egyed
2022 J jnl
Trace Refinement in B and Event-B.
CoRR
Sebastian Stock, Atif Mashkoor, Michael Leuschel, Alexander Egyed
2021 C conf
Improving SMT Solver Integrations for the Validation of B and Event-B Models.
FMICS
Joshua Schmidt, Michael Leuschel
2021 J jnl
Integrating formal specifications into applications: the ProB Java API.
Formal Methods Syst. Des.
Philipp Körner, Jens Bendisposto, Jannik Dunkelau, Sebastian Krings, Michael Leuschel
2021 C conf
ProB2-UI: A Java-Based User Interface for ProB.
FMICS
Jens Bendisposto, David Geleßus, Yumiko Jansing, Michael Leuschel, Antonia Pütz, Fabian Vu, Michelle Werth
2021 — conf
Spot the Difference: A Detailed Comparison Between B and Event-B.
Logic, Computation and Rigorous Methods
Michael Leuschel
2021 — conf
Validation Obligations: A Novel Approach to Check Compliance between Requirements and their Formal Specification.
ICSE (NIER)
Atif Mashkoor, Michael Leuschel, Alexander Egyed
2021 J jnl
Validation Obligations: A Novel Approach to Check Compliance between Requirements and their Formal Specification.
CoRR
Atif Mashkoor, Michael Leuschel, Alexander Egyed
2021 C conf
Validation of Formal Models by Timed Probabilistic Simulation.
ABZ
Fabian Vu, Michael Leuschel, Atif Mashkoor
2020 C conf
Analysing ProB's Constraint Solving Backends - What Do They Know? Do They Know Things? Let's Find Out!
ABZ
Jannik Dunkelau, Joshua Schmidt, Michael Leuschel
2020 B conf
Fast and Effective Well-Definedness Checking.
IFM
Michael Leuschel
2020 C conf
Modelling and Validating an Automotive System in Classical B and Event-B.
ABZ
Michael Leuschel, Mareike Mutz, Michelle Werth
2020 — conf
On the Performance of Bytecode Interpreters in Prolog.
WFLP
Philipp Körner, David Schneider, Michael Leuschel
2020 J jnl
On the Performance of Bytecode Interpreters in Prolog.
CoRR
Philipp Körner, David Schneider, Michael Leuschel
2020 C conf
ProB and Jupyter for Logic, Set Theory, Theoretical Computer Science and Formal Methods.
ABZ
David Geleßus, Michael Leuschel
2020 — conf
Prolog for Verification, Analysis and Transformation Tools.
VPT/HCVS@ETAPS
Michael Leuschel
2020 C conf
The First Twenty-Five Years of Industrial Use of the B-Method.
FMICS
Michael J. Butler, Philipp Körner, Sebastian Krings, Thierry Lecomte, Michael Leuschel, Luis-Fernando Mejia, Laurent Voisin
2020 C conf
Towards a Shared Specification Repository.
ABZ
Philipp Körner, Michael Leuschel, Jannik Dunkelau
2020 J jnl
Translating Alloy and extensions to classical B.
Sci. Comput. Program.
Sebastian Krings, Michael Leuschel, Joshua Schmidt, David Schneider, Marc Frappier
2020 J jnl
Validation and real-life demonstration of ETCS hybrid level 3 principles using a formal B model.
Int. J. Softw. Tools Technol. Transf.
Dominik Hansen, Michael Leuschel, Philipp Körner, Sebastian Krings, Thomas Naulin, Nader Nayeri, David Schneider, Frank Skowron
2020 C conf
VisB: A Lightweight Tool to Visualize Formal Models with SVG Graphics.
ABZ
Michelle Werth, Michael Leuschel
2019 B conf
A Multi-target Code Generator for High-Level B.
IFM
Fabian Vu, Dominik Hansen, Philipp Körner, Michael Leuschel
2019 — conf
Applying Formal Reasoning to Model Transformation: The Meeduse solution.
TTC@STAF
Akram Idani, Germán Vega, Michael Leuschel
2019 B conf
Embedding High-Level Formal Specifications into Applications.
FM
Philipp Körner, Jens Bendisposto, Jannik Dunkelau, Sebastian Krings, Michael Leuschel
2019 B conf
Embedding SMT-LIB into B for Interactive Proof and Constraint Solving.
IFM
Sebastian Krings, Michael Leuschel
2019 — conf
Property-Based Modelling and Validation of a CBTC Zone Controller in Event-B.
RSSRail
Mathieu Comptier, Michael Leuschel, Luis-Fernando Mejia, Julien Molinero Perez, Mareike Mutz
2019 — ch.
Software Architecture of Modern Model Checkers.
Computing and Software Science
Fabrice Kordon, Michael Leuschel, Jaco van de Pol, Yann Thierry-Mieg
2018 C conf
A Translation from Alloy to B.
ABZ
Sebastian Krings, Joshua Schmidt, Carola Brings, Marc Frappier, Michael Leuschel
2018 J jnl
Enabling analysis for Event-B.
Sci. Comput. Program.
Ivaylo Dobrikov, Michael Leuschel
2018 B conf
Extended Algebraic State-Transition Diagrams.
ICECCS
Lionel N. Tidjon, Marc Frappier, Michael Leuschel, Amel Mammar
2018 B conf
Formalisation of SysML/KAOS Goal Assignments with B System Component Decompositions.
IFM
Steve Jeffrey Tueno Fotso, Marc Frappier, Régine Laleau, Amel Mammar, Michael Leuschel
2018 B conf
From Software Specifications to Constraint Programming.
SEFM
Stefan Hallerstede, Miran Hasanagic, Sebastian Krings, Peter Gorm Larsen, Michael Leuschel
2018 J jnl
Model-based problem solving for university timetable validation and improvement.
Formal Aspects Comput.
David Schneider, Michael Leuschel, Tobias Witt
2018 J jnl
Proof assisted bounded and unbounded symbolic model checking of software and system models.
Sci. Comput. Program.
Sebastian Krings, Michael Leuschel
2018 B conf
Repair and Generation of Formal Models Using Synthesis.
IFM
Joshua Schmidt, Sebastian Krings, Michael Leuschel
2018 — conf
Solving Set Constraints in B and Event-B: Foundations and Applications (invited talk).
SETS@ABZ
Michael Leuschel
2018 B conf
State-of-the-Art Model Checking for B and Event-B Using ProB and LTSmin.
IFM
Philipp Körner, Michael Leuschel, Jeroen Meijer
2018 C conf
Three Is a Crowd: SAT, SMT and CLP on a Chessboard.
PADL
Sebastian Krings, Michael Leuschel, Philipp Körner, Stefan Hallerstede, Miran Hasanagic
2018 C conf
Using a Formal B Model at Runtime in a Demonstration of the ETCS Hybrid Level 3 Concept with Real Trains.
ABZ
Dominik Hansen, Michael Leuschel, David Schneider, Sebastian Krings, Philipp Körner, Thomas Naulin, Nader Nayeri, Frank Skowron
2017 — conf
Constraint Logic Programming over Infinite Domains with an Application to Proof.
WLP / WFLP
Sebastian Krings, Michael Leuschel
2017 J jnl
Inferring physical units in formal models.
Softw. Syst. Model.
Sebastian Krings, Michael Leuschel
2017 J jnl
Validation of the ABZ landing gear system using ProB.
Int. J. Softw. Tools Technol. Transf.
Lukas Ladenberger, Dominik Hansen, Harald Wiegard, Jens Bendisposto, Michael Leuschel
2016 C conf
A Compact Encoding of Sequential ASMs in Event-B.
ABZ
Michael Leuschel, Egon Börger
2016 B conf
BMotionWeb: A Tool for Rapid Creation of Formal Prototypes.
SEFM
Lukas Ladenberger, Michael Leuschel
2016 C conf
Enabling Analysis for Event-B.
ABZ
Ivaylo Dobrikov, Michael Leuschel
2016 — conf
Formal Model-Based Constraint Solving and Document Generation.
SBMF
Michael Leuschel
2016 C conf
Generating Event-B Specifications from Algorithm Descriptions.
ABZ
Joy Clark, Jens Bendisposto, Stefan Hallerstede, Dominik Hansen, Michael Leuschel
2016 C conf
Interactive Model Repair by Synthesis.
ABZ
Joshua Schmidt, Sebastian Krings, Michael Leuschel
2016 J jnl
Knowledge Representation Analysis of Graph Mining.
CoRR
Matthias van der Hallen, Sergey Paramonov, Michael Leuschel, Gerda Janssens
2016 B conf
LTL Model Checking under Fairness in ProB.
SEFM
Ivaylo Dobrikov, Michael Leuschel, Daniel Plagge
2016 J jnl
Optimising the ProB model checker for B using partial order reduction.
Formal Aspects Comput.
Ivaylo Dobrikov, Michael Leuschel
2016 C conf
Proof Assisted Symbolic Model Checking for B and Event-B.
ABZ
Sebastian Krings, Michael Leuschel
2016 B conf
SMT Solvers for Validation of B and Event-B Models.
IFM
Sebastian Krings, Michael Leuschel
2016 B conf
Symbolic Reachability Analysis of B Through ProB and LTSmin.
IFM
Jens Bendisposto, Philipp Körner, Michael Leuschel, Jeroen Meijer, Jaco van de Pol, Helen Treharne, Jorden Whitefield
2016 J jnl
Symbolic Reachability Analysis of B through ProB and LTSmin.
CoRR
Jens Bendisposto, Philipp Koerner, Michael Leuschel, Jeroen Meijer, Jaco van de Pol, Helen Treharne, Jorden Whitefield
2016 J jnl
Translating B to TLA
Sci. Comput. Program.
Dominik Hansen, Michael Leuschel
2016 C conf
Using B and ProB for Data Validation Projects.
ABZ
Dominik Hansen, David Schneider, Michael Leuschel
2015 B conf
From Failure to Proof: The ProB Disprover for B and Event-B.
SEFM
Sebastian Krings, Jens Bendisposto, Michael Leuschel
2015 C conf
Mastering the Visualization of Larger State Spaces with Projection Diagrams.
ICFEM
Lukas Ladenberger, Michael Leuschel
2015 B conf
Model-Based Problem Solving for University Timetable Validation and Improvement.
FM
David Schneider, Michael Leuschel, Tobias Witt
2015 B conf
Model-Based Robustness Testing in Event-B Using Mutation.
SEFM
Aymerick Savary, Marc Frappier, Michael Leuschel, Jean-Louis Lanet
2014 — conf
An Approach for Creating Domain Specific Visualisations of CSP Models.
SEFM Workshops
Lukas Ladenberger, Ivaylo Dobrikov, Michael Leuschel
2014 — conf
Checking Computations of Formal Method Tools - A Secondary Toolchain for ProB.
F-IDE
John Witulski, Michael Leuschel
2014 J jnl
Fast offline partial evaluation of logic programs.
Inf. Comput.
Michael Leuschel, Germán Vidal
2014 J jnl
Introduction to the 30th International Conference on Logic Programming Special Issue.
Theory Pract. Log. Program.
Michael Leuschel, Tom Schrijvers
2014 B conf
Optimising the ProB Model Checker for B Using Partial Order Reduction.
SEFM
Ivaylo Dobrikov, Michael Leuschel
2014 J jnl
Preface of Automated Verification of Critical Systems 2010 (AVoCS 2010).
Sci. Comput. Program.
Jens Bendisposto, Michael Leuschel, Markus Roggenbach
2014 C conf
Towards B as a High-Level Constraint Modelling Language - Solving the Jobs Puzzle Challenge.
ABZ
Michael Leuschel, David Schneider
2014 — conf
Towards Constraint-Solving over Higher-Order Unbounded Datatypes using Formal Methods Tools.
VPT@CAV
Michael Leuschel
2014 C conf
Translating B to TLA + for Validation with TLC.
ABZ
Dominik Hansen, Michael Leuschel
2014 — conf
Validation of the ABZ Landing Gear System Using ProB.
ABZ (Case Study)
Dominik Hansen, Lukas Ladenberger, Harald Wiegard, Jens Bendisposto, Michael Leuschel
2014 — conf
Who watches the watchers: Validating the ProB Validation Tool.
F-IDE
Jens Bendisposto, Sebastian Krings, Michael Leuschel
2013 — ch.
Improving Railway Data Validation with ProB.
Industrial Deployment of System Engineering Methods
Jérôme Falampin, Hung Le-Dang, Michael Leuschel, Mikael Mokrani, Daniel Plagge
2013 B conf
Inferring Physical Units in B Models.
SEFM
Sebastian Krings, Michael Leuschel
2013 J jnl
Integration of Tools for Rigorous Software Construction and Analysis (Dagstuhl Seminar 13372).
Dagstuhl Reports
Uwe Glässer, Stefan Hallerstede, Michael Leuschel, Elvinia Riccobene
2013 J jnl
Validation of formal models by refinement animation.
Sci. Comput. Program.
Stefan Hallerstede, Michael Leuschel, Daniel Plagge
2012 C ed.
Abstract State Machines, Alloy, B, VDM, and Z - Third International Conference, ABZ 2012, Pisa, Italy, June 18-21, 2012. Proceedings
ABZ
John Derrick, John S. Fitzgerald, Stefania Gnesi, Sarfraz Khurshid, Michael Leuschel, Steve Reeves, Elvinia Riccobene
2012 J jnl
Experiments in program verification using Event-B.
Formal Aspects Comput.
Stefan Hallerstede, Michael Leuschel
2012 J jnl
Formally Checking Large Data Sets in the Railways
CoRR
Thierry Lecomte, Lilian Burdy, Michael Leuschel
2012 J jnl
Static slicing of explicitly synchronized languages.
Inf. Comput.
Michael Leuschel, Marisa Llorens, Javier Oliver, Josep Silva, Salvador Tamarit
2012 B conf
Translating TLA + to B for Validation with ProB.
IFM
Dominik Hansen, Michael Leuschel
2012 B conf
Validating B, Z and TLA + Using ProB and Kodkod.
FM
Daniel Plagge, Michael Leuschel
2011 C conf
Allocation removal by partial evaluation in a tracing JIT.
PEPM
Carl Friedrich Bolz, Antonio Cuni, Maciej Fijalkowski, Michael Leuschel, Samuele Pedroni, Armin Rigo
2011 J jnl
Automated property verification for large scale B models with ProB.
Formal Aspects Comput.
Michael Leuschel, Jérôme Falampin, Fabian Fritz, Daniel Plagge
2011 B conf
Automatic Flow Analysis for Event-B.
FASE
Jens Bendisposto, Michael Leuschel
2011 J jnl
Constraint-Based Deadlock Checking of High-Level Specifications
CoRR
Stefan Hallerstede, Michael Leuschel
2011 J jnl
Constraint-based deadlock checking of high-level specifications.
Theory Pract. Log. Program.
Stefan Hallerstede, Michael Leuschel
2011 J jnl
Developing Camille, a text editor for Rodin.
Softw. Pract. Exp.
Jens Bendisposto, Fabian Fritz, Michael Jastram, Michael Leuschel, Ingo Weigelt
2011 C conf
On Fitting a Formal Method into Practice.
ICFEM
Rainer Gmehlich, Katrin Grau, Stefan Hallerstede, Michael Leuschel, Felix Lösch, Daniel Plagge
2011 J jnl
Preface.
Electron. Commun. Eur. Assoc. Softw. Sci. Technol.
Alexander B. Romanovsky, Cliff B. Jones, Jens Bendisposto, Michael Leuschel
2011 — conf
Runtime feedback in a meta-tracing JIT for efficient dynamic languages.
ICOOOLPS@ECOOP
Carl Friedrich Bolz, Antonio Cuni, Maciej Fijalkowski, Michael Leuschel, Samuele Pedroni, Armin Rigo
2011 J jnl
Selected papers on Integrated Formal Methods (iFM09).
Sci. Comput. Program.
Michael Leuschel, Heike Wehrheim
2010 — conf
A Refinement-Based Correctness Proof of Symmetry Reduced Model Checking.
ASM
Edd Turner, Michael J. Butler, Michael Leuschel
2010 — conf
An Approach of Requirements Tracing in Formal Refinement.
VSTTE
Michael Jastram, Stefan Hallerstede, Michael Leuschel, Aryldo G. Russo
2010 J jnl
Avocs2010 Preface.
Electron. Commun. Eur. Assoc. Softw. Sci. Technol.
Jens Bendisposto, Michael Leuschel, Markus Roggenbach
2010 — conf
Directed Model Checking for B: An Evaluation and New Techniques.
SBMF
Michael Leuschel, Jens Bendisposto
2010 J jnl
Efficient approximate verification of B and Z models via symmetry markers.
Ann. Math. Artif. Intell.
Michael Leuschel, Thierry Massart
2010 — ed.
Formal Methods for Components and Objects - 8th International Symposium, FMCO 2009, Eindhoven, The Netherlands, November 4-6, 2009. Revised Selected Papers
FMCO
Frank S. de Boer, Marcello M. Bonsangue, Stefan Hallerstede, Michael Leuschel
2010 — conf
Refinement-Animation for Event-B - Towards a Method of Validation.
ASM
Stefan Hallerstede, Michael Leuschel, Daniel Plagge
2010 J jnl
Seven at one stroke: LTL model checking for high-level specifications in B, Z, CSP, and more.
Int. J. Softw. Tools Technol. Transf.
Daniel Plagge, Michael Leuschel
2010 C conf
Towards a jitting VM for prolog execution.
PPDP
Carl Friedrich Bolz, Michael Leuschel, David Schneider
2009 J jnl
A Semantics-Aware Editing Environment for Prolog in Eclipse
CoRR
Jens Bendisposto, Ian Endrijautzki, Michael Leuschel, David Schneider
2009 — conf
Applying Model Checking to Generate Model-Based Integration Tests from Choreography Models.
TestCom/FATES
Sebastian Wieczorek, Vitaly Kozyura, Andreas Roth, Michael Leuschel, Jens Bendisposto, Daniel Plagge, Ina Schieferdecker
2009 B conf
Automated Property Verification for Large Scale B Models.
FM
Michael Leuschel, Jérôme Falampin, Fabian Fritz, Daniel Plagge
2009 — conf
Fast and Accurate Strong Termination Analysis with an Application to Partial Evaluation.
WFLP
Michael Leuschel, Salvador Tamarit, Germán Vidal
2009 — conf
How to Explain Mistakes.
TFM
Stefan Hallerstede, Michael Leuschel
2009 J jnl
Improving Size-Change Analysis in Offline Partial Evaluation
CoRR
Michael Leuschel, Salvador Tamarit, Germán Vidal
2009 B ed.
Integrated Formal Methods, 7th International Conference, IFM 2009, Düsseldorf, Germany, February 16-19, 2009. Proceedings
IFM
Michael Leuschel, Heike Wehrheim
2009 C conf
Pie Tree Visualization.
SEKE
Mireille Samia, Michael Leuschel
2009 C conf
Proof Assisted Model Checking for B.
ICFEM
Jens Bendisposto, Michael Leuschel
2009 C conf
SOC: a slicer for CSP specifications.
PEPM
Michael Leuschel, Marisa Llorens, Javier Oliver, Josep Silva, Salvador Tamarit
2009 C conf
Towards Just-In-Time Partial Evaluation of Prolog.
LOPSTR
Carl Friedrich Bolz, Michael Leuschel, Armin Rigo
2009 A conf
Towards pie tree visualization of graphs and large software architectures.
ICPC
Mireille Samia, Michael Leuschel
2009 — conf
Validating and Animating Higher-Order Recursive Functions in B.
Rigorous Methods for Software Construction and Analysis
Michael Leuschel, Dominique Cansell, Michael J. Butler
2009 C conf
Visualising Event-B Models with B-Motion Studio.
FMICS
Lukas Ladenberger, Jens Bendisposto, Michael Leuschel
2008 C conf
Declarative programming for verification: lessons and outlook.
PPDP
Michael Leuschel
2008 J jnl
Editorial.
High. Order Symb. Comput.
Julia Lawall, Michael Leuschel, Peter Sestoft
2008 J jnl
Efficient and flexible access control via Jones-optimal logic program specialisation.
High. Order Symb. Comput.
Steve Barker, Michael Leuschel, Mauricio Varea
2008 C conf
Fast Offline Partial Evaluation of Large Logic Programs.
LOPSTR
Michael Leuschel, Germán Vidal
2008 J jnl
La validation de modèles Event-B avec le plug-in ProB pour RODIN.
Tech. Sci. Informatiques
Jens Bendisposto, Michael Leuschel, O. Ligot, Mireille Samia
2008 Misc conf
ProB gets Nauty: Effective Symmetry Reduction for B and Z Models.
TASE
Corinna Spermann, Michael Leuschel
2008 J jnl
ProB: an automated analysis toolset for the B method.
Int. J. Softw. Tools Technol. Transf.
Michael Leuschel, Michael J. Butler
2008 C conf
Probing the Depths of CSP-M: A New fdr-Compliant Validation Tool.
ICFEM
Michael Leuschel, Marc Fontaine
2008 C conf
The High Road to Formal Validation: .
ABZ
Michael Leuschel
2008 C conf
The MEB and CEB Static Analysis for CSP Specifications.
LOPSTR
Michael Leuschel, Marisa Llorens, Javier Oliver, Josep Silva, Salvador Tamarit
2008 — conf
Towards Demonstrably Correct Compilation of Java Byte Code.
FMCO
Michael Leuschel
2007 — conf
A Generic Flash-Based Animation Engine for ProB.
B
Jens Bendisposto, Michael Leuschel
2007 — conf
Animating and Model Checking B Specifications with Higher-Order Recursive Functions.
Rigorous Methods for Software Construction and Analysis
Michael Leuschel, Jens Bendisposto
2007 C conf
Automatic Testing from Formal Specifications.
TAP
Manoranjan Satpathy, Michael J. Butler, Michael Leuschel, S. Ramesh
2007 — conf
BE
B
Jens Bendisposto, Michael Leuschel
2007 B conf
Efficient Approximate Verification of Promela Models Via Symmetry Markers.
ATVA
Dragan Bosnacki, Alastair F. Donaldson, Michael Leuschel, Thierry Massart
2007 C conf
Partial Evaluation of Pointcuts.
PADL
Karl Klose, Klaus Ostermann, Michael Leuschel
2007 C ed.
Proceedings of the 9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, July 14-16, 2007, Wroclaw, Poland
PPDP
Michael Leuschel, Andreas Podelski
2007 C conf
Seven at one stroke: LTL model checking for High-level Specifications in B, Z, CSP, and more.
ISoLA
Michael Leuschel, Daniel Plagge
2007 Misc conf
Symmetry Reduced Model Checking for B.
TASE
Edd Turner, Michael Leuschel, Corinna Spermann, Michael J. Butler
2007 — conf
Symmetry Reduction for B by Permutation Flooding.
B
Michael Leuschel, Michael J. Butler, Corinna Spermann, Edd Turner
2007 B conf
Validating Z Specifications Using the ProBAnimator and Model Checker.
IFM
Daniel Plagge, Michael Leuschel
2006 J jnl
Rapid Visualization of B Specifications containing Higher-Order Recursive Functions.
Softwaretechnik-Trends
Jens Bendisposto, Michael Leuschel
2006 C conf
Supervising Offline Partial Evaluation of Logic Programs Using Online Techniques.
LOPSTR
Michael Leuschel, Stephen-John Craig, Daniel Elphick
2006 C conf
The Ecce and Logen partial evaluators and their web interfaces.
PEPM
Michael Leuschel, Daniel Elphick, Mauricio Varea, Stephen-John Craig, Marc Fontaine
2005 C conf
Automatic Refinement Checking for B.
ICFEM
Michael Leuschel, Michael J. Butler
2005 B conf
Combining CSP and B for Specification and Property Verification.
FM
Michael J. Butler, Michael Leuschel
2005 A conf
Forward Slicing by Conjunctive Partial Deduction and Argument Filtering.
ESOP
Michael Leuschel, Germán Vidal
2005 J jnl
Guest Editorial.
Formal Aspects Comput.
Michael Leuschel
2005 C conf
Self-tuning resource aware specialisation for prolog.
PPDP
Stephen-John Craig, Michael Leuschel
2005 — conf
Tools for System Validation with B Abstract Machines.
Abstract State Machines
Michael J. Butler, Michael Leuschel, Colin F. Snook
2005 C conf
Towards Provably Correct Code Generation via Horn Logical Continuation Semantics.
PADL
Qian Wang, Gopal Gupta, Michael Leuschel
2005 — conf
Visualising Larger State Spaces in Pro B.
ZB
Michael Leuschel, Edd Turner
2004 — conf
A Trust Analysis Methodology for Pervasive Computing Systems.
Trusting Agents for Trusting Electronic Societies
Stéphane Lo Presti, Michael J. Butler, Michael Leuschel, Chris Booth
2004 J jnl
A framework for the integration of partial evaluation and abstract interpretation of logic programs.
ACM Trans. Program. Lang. Syst.
Michael Leuschel
2004 — ch.
Binding-Time Analysis for Mercury.
Program Development in Computational Logic
Wim Vanhoof, Maurice Bruynooghe, Michael Leuschel
2004 C conf
Efficient and flexible access control via logic program specialisation.
PEPM
Steve Barker, Michael Leuschel, Mauricio Varea
2004 C conf
Fully Automatic Binding-Time Analysis for Prolog.
LOPSTR
Stephen-John Craig, John P. Gallagher, Michael Leuschel, Kim S. Henriksen
2004 J jnl
Introduction to the Special Issue on Verification and Computational Logic.
Theory Pract. Log. Program.
Michael Leuschel, Andreas Podelski, C. R. Ramakrishnan, Ulrich Ultes-Nitsche
2004 Misc conf
LIX: an Effective Self-applicable Partial Evaluator for Prolog.
FLOPS
Stephen-John Craig, Michael Leuschel
2004 C conf
Model checking object petri nets in prolog.
PPDP
Berndt Farwer, Michael Leuschel
2004 J jnl
Offline specialisation in Prolog using a hand-written compiler generator.
Theory Pract. Log. Program.
Michael Leuschel, Jesper Jørgensen, Wim Vanhoof, Maurice Bruynooghe
2004 — conf
PROB: un outil de modélisation formelle.
JFPLC
Michael Leuschel
2004 — conf
ProTest: An Automatic Test Environment for B Specifications.
MBT
Manoranjan Satpathy, Michael Leuschel, Michael J. Butler
2004 — ch.
Specialising Interpreters Using Offline Partial Deduction.
Program Development in Computational Logic
Michael Leuschel, Stephen-John Craig, Maurice Bruynooghe, Wim Vanhoof
2004 — conf
The Use of Formal Methods in the Analysis of Trust (Position Paper).
iTrust
Michael J. Butler, Michael Leuschel, Stéphane Lo Presti, Phillip Turner
2003 — conf
A Compiler Generator for Constraint Logic Programs.
Ershov Memorial Conference
Stephen-John Craig, Michael Leuschel
2003 C conf
Inductive Theorem Proving by Program Specialisation: Generating Proofs for Isabelle Using Ecce.
LOPSTR
Helko Lehmann, Michael Leuschel
2003 C ed.
Logic Based Program Synthesis and Tranformation, 12th International Workshop, LOPSTR 2002, Madrid, Spain, September 17-20,2002, Revised Selected Papers
LOPSTR
Michael Leuschel
2003 — conf
Model-Based Approaches for Validating Business Critical Systems.
STEP
Juan Carlos Augusto, Yvonne Howard, Andrew M. Gravell, Carla Ferreira, Stefan Gruner, Michael Leuschel
2003 B conf
Partial Evaluation of MATLAB.
GPCE
Daniel Elphick, Michael Leuschel, Simon J. Cox
2003 — conf
ProB: A Model Checker for B.
FME
Michael Leuschel, Michael J. Butler
2003 C ed.
Proceedings of the 2003 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, 2003, San Diego, California, USA, June 7, 2003
PEPM
Michael Leuschel
2003 — conf
The Benefits of Rapid Modelling for E-business System Development.
ER (Workshops)
Juan Carlos Augusto, Carla Ferreira, Andrew M. Gravell, Michael Leuschel, Karen M. Y. Ng
2002 J jnl
Book Reviews.
Softw. Test. Verification Reliab.
Michael Leuschel
2002 — conf
Homeomorphic Embedding for Online Termination of Symbolic Methods.
The Essence of Computation
Michael Leuschel
2002 J jnl
Logic program specialisation through partial deduction: Control issues
CoRR
Michael Leuschel, Maurice Bruynooghe
2002 J jnl
Logic program specialisation through partial deduction: Control issues.
Theory Pract. Log. Program.
Michael Leuschel, Maurice Bruynooghe
2002 J jnl
Offline Specialisation in Prolog Using a Hand-Written Compiler Generator
CoRR
Michael Leuschel, Jesper Jørgensen, Wim Vanhoof, Maurice Bruynooghe
2001 C conf
Abstract Conjunctive Partial Deduction Using Regular Types and Its Application to Model Checking.
LOPSTR
Michael Leuschel, Stefan Gruner
2001 C conf
Design and Implementation of the High-Level Specification Language CSP(LP) in Prolog.
PADL
Michael Leuschel
2001 — conf
How to Make FDR Spin LTL Model Checking of CSP by Refinement.
FME
Michael Leuschel, Thierry Massart, Andrew Currie
2000 J jnl
A Polyvariant Binding-Time Analysis for Off-line Partial Deduction
CoRR
Maurice Bruynooghe, Michael Leuschel, Konstantinos Sagonas
2000 — conf
Coverability of Reset Petri Nets and Other Well-Structured Transition Systems by Partial Deduction.
Computational Logic
Michael Leuschel, Helko Lehmann
2000 — conf
Decidability Results for the Propositional Fluent Calculus.
Computational Logic
Helko Lehmann, Michael Leuschel
2000 J jnl
Erratum to: "Conjunctive Partial Deduction: Foundations, Control, Algorithms and Experiments".
J. Log. Program.
Danny De Schreye, Robert Glück, Jesper Jørgensen, Michael Leuschel, Bern Martens, Morten Heine Sørensen
2000 B conf
Solving Planning Problems by Partial Deduction.
LPAR
Helko Lehmann, Michael Leuschel
2000 C conf
Solving coverability problems of petri nets by partial deduction.
PPDP
Michael Leuschel, Helko Lehmann
1999 — conf
Abstraction-Based Partial Deduction for Solving Inverse Problems - A Transformational Approach to Software Verification.
Ershov Memorial Conference
Robert Glück, Michael Leuschel
1999 J jnl
Conjunctive Partial Deduction: Foundations, Control, Algorithms, and Experiments.
J. Log. Program.
Danny De Schreye, Robert Glück, Jesper Jørgensen, Michael Leuschel, Bern Martens, Morten Heine Sørensen
1999 — conf
Efficient Specialisation in Prolog Using the Hand-Written Compiler Generator LOGEN.
WOID@ICLP
Michael Leuschel, Jesper Jørgensen
1999 C conf
Infinite State Model Checking by Abstract Interpretation and Program Specialisation.
LOPSTR
Michael Leuschel, Thierry Massart
1999 — conf
Preface - Workshop on Optimization and Implementation of Declarative Programs.
WOID@ICLP
Michael Leuschel
1999 — conf
Sonic Partial Deduction.
Ershov Memorial Conference
Jonathan C. Martin, Michael Leuschel
1999 — ed.
Workshop on Optimization and Implementation of Declarative Programs, WOID 1999, in connection with the International Conference on Logic Programming, ICLP 1999, Las Cruces, New Mexico, USA, December 2-3, 1999
WOID@ICLP
Michael Leuschel
1998 A conf
A Polyvariant Binding-Time Analysis for Off-line Partial Deduction.
ESOP
Maurice Bruynooghe, Michael Leuschel, Konstantinos Sagonas
1998 — conf
Advanced Logic Program Specialisation.
Partial Evaluation
Michael Leuschel
1998 J jnl
Constrained Partial Deduction and the Preservation of Characteristic Trees.
New Gener. Comput.
Michael Leuschel, Danny De Schreye
1998 J jnl
Controlling Generalization amd Polyvariance in Partial Deduction of Normal Logic Programs.
ACM Trans. Program. Lang. Syst.
Michael Leuschel, Bern Martens, Danny De Schreye
1998 J jnl
Creating Specialised Integrity Checks Through Partial Evaluation of Meta-Interpreters.
J. Log. Program.
Michael Leuschel, Danny De Schreye
1998 J jnl
Extending Partial Deduction to Tabled Execution: Some Results and Open Issues.
ACM Comput. Surv.
Konstantinos Sagonas, Michael Leuschel
1998 C conf
Improving Homeomorphic Embedding for Online Termination.
LOPSTR
Michael Leuschel
1998 — conf
Logic Program Specialisation.
Partial Evaluation
Michael Leuschel
1998 B conf
On the Power of Homeomorphic Embedding for Online Termination.
SAS
Michael Leuschel
1998 — conf
Program Specialisation and Abstract Interpretation Reconciled.
IJCSLP
Michael Leuschel
1998 J jnl
Some Achievements and Prospects in Partial Deduction.
ACM Comput. Surv.
Michael Leuschel, Bern Martens, Danny De Schreye
1997 J jnl
Advanced Techniques for Logic Program Specialisation.
AI Commun.
Michael Leuschel
1997 — conf
Constrained Partial Deduction.
WLP
Michael Leuschel, Danny De Schreye
1997 — conf
Extending Homeomorphic Embedding in the Context of Logic Programming.
WLP
Michael Leuschel
1997 C conf
Preserving Termination of Tabled Logic Programs While Unfolding.
LOPSTR
Michael Leuschel, Bern Martens, Konstantinos Sagonas
1997 — conf
Specialization of Declarative Programs and Its Applications (Workshop Overview).
ILPS
Michael Leuschel
1997 C conf
Termination Analysis for Tabled Logic Programming.
LOPSTR
Stefaan Decorte, Danny De Schreye, Michael Leuschel, Bern Martens, Konstantinos Sagonas
1996 — conf
A Conceptual Embedding of Folding into Partial Deduction: Towards a Maximal Integration.
JICSLP
Michael Leuschel, Danny De Schreye, D. Andre de Waal
1996 C conf
Conjunctive Partial Deduction in Practice.
LOPSTR
Jesper Jørgensen, Michael Leuschel, Bern Martens
1996 — conf
Efficiently Generating Efficient Generating Extensions in Prolog.
Dagstuhl Seminar on Partial Evaluation
Jesper Jørgensen, Michael Leuschel
1996 — conf
Global Control for Partial Deduction through Characteristic Atoms and Global Trees.
Dagstuhl Seminar on Partial Evaluation
Michael Leuschel, Bern Martens
1996 — conf
Logic Program Specialisation: How To Be More Specific.
PLILP
Michael Leuschel, Danny De Schreye
1996 C conf
Logic Program Specialisation: How to Be More Specific (Abstract).
LOPSTR
Michael Leuschel, Danny De Schreye
1996 C conf
Redundant Argument Filtering of Logic Programs.
LOPSTR
Michael Leuschel, Morten Heine Sørensen
1995 C conf
Ecological Partial Deduction: Preserving Characteristic Trees Without Constraints.
LOPSTR
Michael Leuschel
1995 — conf
Generating Specialised Update Procedures Through Partial Deduction of the Ground Representation.
Deductive Databases / Abduction in Deductive Databases
Michael Leuschel, Bern Martens
1995 — conf
Partial Deduction of the Ground Representation and its Application to Integrity Checking.
ILPS
Michael Leuschel, Bern Martens
1995 C conf
Towards Creating Specialised Integrity Checks through Partial Evaluation of Meta-Interpreters.
PEPM
Michael Leuschel, Danny De Schreye
1995 — conf
Tutorial on Program Specialisation (Abstract).
ILPS
Danny De Schreye, Michael Leuschel, Bern Martens
1994 C conf
Partial Evaluation of the "Real Thing".
LOPSTR
Michael Leuschel