| 2026 | PADL | Using Prolog to Translate Set Theory and B to SAT. | Michael Leuschel |
| 2025 | FMICS | Promise-Driven Modeling: A Structured Approach for Modeling Cyber-Physical Systems. | Felix Schaber, Atif Mashkoor, Michael Leuschel |
| 2025 | TASE | Failure Divergence Refinement for Event-B. | Sebastian Stock, Michael Leuschel, Atif Mashkoor |
| 2024 | FM | B2SAT: A Bare-Metal Reduction of B to SAT. | Michael Leuschel |
| 2024 | ICECCS | Validation of RailML Using ProB. | Jan Gruteser, Michael Leuschel |
| 2024 | KI | Evaluating AI-Based Components in Autonomous Railway Systems - A Methodology. | Jan Robach, Oliver De Candido, Ahmed Hammam, Michael Leuschel |
| 2023 | IFM | Performance Fuzzing with Reinforcement-Learning and Well-Defined Constraints for the B Method. | Jannik Dunkelau, Michael Leuschel |
| 2022 | FMICS | Generating Domain-Specific Interactive Validation Documents. | Fabian Vu, Christopher Happe, Michael Leuschel |
| 2022 | ICFEM | Trace Refinement in B and Event-B. | Sebastian Stock, Atif Mashkoor, Michael Leuschel, Alexander Egyed |
| 2022 | ICFEM | Model Checking B Models via High-Level Code Generation. | Fabian Vu, Dominik Brandt, Michael Leuschel |
| 2022 | IFM | Operation Caching and State Compression for Model Checking of High-Level Models - How to Have Your Cake and Eat It. | Michael Leuschel |
| 2021 | FMICS | ProB2-UI: A Java-Based User Interface for ProB. | Jens Bendisposto, David Geleus, Yumiko Jansing, Michael Leuschel, Antonia Ptz, Fabian Vu, Michelle Werth |
| 2021 | FMICS | Improving SMT Solver Integrations for the Validation of B and Event-B Models. | Joshua Schmidt, Michael Leuschel |
| 2021 | ICSE | Validation Obligations: A Novel Approach to Check Compliance between Requirements and their Formal Specification. | Atif Mashkoor, Michael Leuschel, Alexander Egyed |
| 2020 | FMICS | The First Twenty-Five Years of Industrial Use of the B-Method. | Michael J. Butler, Philipp Krner, Sebastian Krings, Thierry Lecomte, Michael Leuschel, Luis-Fernando Mejia, Laurent Voisin |
| 2020 | IFM | Fast and Effective Well-Definedness Checking. | Michael Leuschel |
| 2019 | FM | Embedding High-Level Formal Specifications into Applications. | Philipp Krner, Jens Bendisposto, Jannik Dunkelau, Sebastian Krings, Michael Leuschel |
| 2019 | IFM | Embedding SMT-LIB into B for Interactive Proof and Constraint Solving. | Sebastian Krings, Michael Leuschel |
| 2019 | IFM | A Multi-target Code Generator for High-Level B. | Fabian Vu, Dominik Hansen, Philipp Krner, Michael Leuschel |
| 2018 | ICECCS | Extended Algebraic State-Transition Diagrams. | Lionel N. Tidjon, Marc Frappier, Michael Leuschel, Amel Mammar |
| 2018 | IFM | Formalisation of SysML/KAOS Goal Assignments with B System Component Decompositions. | Steve Jeffrey Tueno Fotso, Marc Frappier, Rgine Laleau, Amel Mammar, Michael Leuschel |
| 2018 | IFM | State-of-the-Art Model Checking for B and Event-B Using ProB and LTSmin. | Philipp Krner, Michael Leuschel, Jeroen Meijer |
| 2018 | IFM | Repair and Generation of Formal Models Using Synthesis. | Joshua Schmidt, Sebastian Krings, Michael Leuschel |
| 2018 | PADL | Three Is a Crowd: SAT, SMT and CLP on a Chessboard. | Sebastian Krings, Michael Leuschel, Philipp Krner, Stefan Hallerstede, Miran Hasanagic |
| 2018 | SEFM | From Software Specifications to Constraint Programming. | Stefan Hallerstede, Miran Hasanagic, Sebastian Krings, Peter Gorm Larsen, Michael Leuschel |
| 2016 | IFM | Symbolic Reachability Analysis of B Through ProB and LTSmin. | Jens Bendisposto, Philipp Krner, Michael Leuschel, Jeroen Meijer, Jaco van de Pol, Helen Treharne, Jorden Whitefield |
| 2016 | IFM | SMT Solvers for Validation of B and Event-B Models. | Sebastian Krings, Michael Leuschel |
| 2016 | SEFM | LTL Model Checking under Fairness in ProB. | Ivaylo Dobrikov, Michael Leuschel, Daniel Plagge |
| 2016 | SEFM | BMotionWeb: A Tool for Rapid Creation of Formal Prototypes. | Lukas Ladenberger, Michael Leuschel |
| 2015 | FM | Model-Based Problem Solving for University Timetable Validation and Improvement. | David Schneider, Michael Leuschel, Tobias Witt |
| 2015 | ICFEM | Mastering the Visualization of Larger State Spaces with Projection Diagrams. | Lukas Ladenberger, Michael Leuschel |
| 2015 | SEFM | From Failure to Proof: The ProB Disprover for B and Event-B. | Sebastian Krings, Jens Bendisposto, Michael Leuschel |
| 2015 | SEFM | Model-Based Robustness Testing in Event-B Using Mutation. | Aymerick Savary, Marc Frappier, Michael Leuschel, Jean-Louis Lanet |
| 2014 | CAV | Towards Constraint-Solving over Higher-Order Unbounded Datatypes using Formal Methods Tools. | Michael Leuschel |
| 2014 | SEFM | Optimising the ProB Model Checker for B Using Partial Order Reduction. | Ivaylo Dobrikov, Michael Leuschel |
| 2014 | SEFM | An Approach for Creating Domain Specific Visualisations of CSP Models. | Lukas Ladenberger, Ivaylo Dobrikov, Michael Leuschel |
| 2013 | SEFM | Inferring Physical Units in B Models. | Sebastian Krings, Michael Leuschel |
| 2012 | FM | Validating B, Z and TLA + Using ProB and Kodkod. | Daniel Plagge, Michael Leuschel |
| 2012 | IFM | Translating TLA + to B for Validation with ProB. | Dominik Hansen, Michael Leuschel |
| 2011 | ECOOP | Runtime feedback in a meta-tracing JIT for efficient dynamic languages. | Carl Friedrich Bolz, Antonio Cuni, Maciej Fijalkowski, Michael Leuschel, Samuele Pedroni, Armin Rigo |
| 2011 | FASE | Automatic Flow Analysis for Event-B. | Jens Bendisposto, Michael Leuschel |
| 2011 | ICFEM | On Fitting a Formal Method into Practice. | Rainer Gmehlich, Katrin Grau, Stefan Hallerstede, Michael Leuschel, Felix Lsch, Daniel Plagge |
| 2011 | PEPM | Allocation removal by partial evaluation in a tracing JIT. | Carl Friedrich Bolz, Antonio Cuni, Maciej Fijalkowski, Michael Leuschel, Samuele Pedroni, Armin Rigo |
| 2010 | PPDP | Towards a jitting VM for prolog execution. | Carl Friedrich Bolz, Michael Leuschel, David Schneider |
| 2009 | FM | Automated Property Verification for Large Scale B Models. | Michael Leuschel, Jrme Falampin, Fabian Fritz, Daniel Plagge |
| 2009 | FMICS | Visualising Event-B Models with B-Motion Studio. | Lukas Ladenberger, Jens Bendisposto, Michael Leuschel |
| 2009 | ICFEM | Proof Assisted Model Checking for B. | Jens Bendisposto, Michael Leuschel |
| 2009 | LOPSTR | Towards Just-In-Time Partial Evaluation of Prolog. | Carl Friedrich Bolz, Michael Leuschel, Armin Rigo |
| 2009 | PEPM | SOC: a slicer for CSP specifications. | Michael Leuschel, Marisa Llorens, Javier Oliver, Josep Silva, Salvador Tamarit |
| 2009 | SEKE | Pie Tree Visualization. | Mireille Samia, Michael Leuschel |
| 2008 | ICFEM | Probing the Depths of CSP-M: A New fdr-Compliant Validation Tool. | Michael Leuschel, Marc Fontaine |
| 2008 | LOPSTR | The MEB and CEB Static Analysis for CSP Specifications. | Michael Leuschel, Marisa Llorens, Javier Oliver, Josep Silva, Salvador Tamarit |
| 2008 | LOPSTR | Fast Offline Partial Evaluation of Large Logic Programs. | Michael Leuschel, Germn Vidal |
| 2008 | PPDP | Declarative programming for verification: lessons and outlook. | Michael Leuschel |
| 2008 | TASE | ProB gets Nauty: Effective Symmetry Reduction for B and Z Models. | Corinna Spermann, Michael Leuschel |
| 2007 | ATVA | Efficient Approximate Verification of Promela Models Via Symmetry Markers. | Dragan Bosnacki, Alastair F. Donaldson, Michael Leuschel, Thierry Massart |
| 2007 | IFM | Validating Z Specifications Using the ProBAnimator and Model Checker. | Daniel Plagge, Michael Leuschel |
| 2007 | ISoLA | Seven at one stroke: LTL model checking for High-level Specifications in B, Z, CSP, and more. | Michael Leuschel, Daniel Plagge |
| 2007 | PADL | Partial Evaluation of Pointcuts. | Karl Klose, Klaus Ostermann, Michael Leuschel |
| 2007 | TAP | Automatic Testing from Formal Specifications. | Manoranjan Satpathy, Michael J. Butler, Michael Leuschel, S. Ramesh |
| 2007 | TASE | Symmetry Reduced Model Checking for B. | Edd Turner, Michael Leuschel, Corinna Spermann, Michael J. Butler |
| 2006 | LOPSTR | Supervising Offline Partial Evaluation of Logic Programs Using Online Techniques. | Michael Leuschel, Stephen-John Craig, Daniel Elphick |
| 2006 | PEPM | The Ecce and Logen partial evaluators and their web interfaces. | Michael Leuschel, Daniel Elphick, Mauricio Varea, Stephen-John Craig, Marc Fontaine |
| 2005 | ESOP | Forward Slicing by Conjunctive Partial Deduction and Argument Filtering. | Michael Leuschel, Germn Vidal |
| 2005 | FM | Combining CSP and B for Specification and Property Verification. | Michael J. Butler, Michael Leuschel |
| 2005 | ICFEM | Automatic Refinement Checking for B. | Michael Leuschel, Michael J. Butler |
| 2005 | PADL | Towards Provably Correct Code Generation via Horn Logical Continuation Semantics. | Qian Wang, Gopal Gupta, Michael Leuschel |
| 2005 | PPDP | Self-tuning resource aware specialisation for prolog. | Stephen-John Craig, Michael Leuschel |
| 2004 | FLOPS | LIX: an Effective Self-applicable Partial Evaluator for Prolog. | Stephen-John Craig, Michael Leuschel |
| 2004 | LOPSTR | Fully Automatic Binding-Time Analysis for Prolog. | Stephen-John Craig, John P. Gallagher, Michael Leuschel, Kim S. Henriksen |
| 2004 | PEPM | Efficient and flexible access control via logic program specialisation. | Steve Barker, Michael Leuschel, Mauricio Varea |
| 2004 | PPDP | Model checking object petri nets in prolog. | Berndt Farwer, Michael Leuschel |
| 2003 | ER | The Benefits of Rapid Modelling for E-business System Development. | Juan Carlos Augusto, Carla Ferreira, Andrew M. Gravell, Michael Leuschel, Karen M. Y. Ng |
| 2003 | FM | ProB: A Model Checker for B. | Michael Leuschel, Michael J. Butler |
| 2003 | GPCE | Partial Evaluation of MATLAB. | Daniel Elphick, Michael Leuschel, Simon J. Cox |
| 2003 | LOPSTR | Inductive Theorem Proving by Program Specialisation: Generating Proofs for Isabelle Using Ecce. | Helko Lehmann, Michael Leuschel |
| 2001 | FM | How to Make FDR Spin LTL Model Checking of CSP by Refinement. | Michael Leuschel, Thierry Massart, Andrew Currie |
| 2001 | LOPSTR | Abstract Conjunctive Partial Deduction Using Regular Types and Its Application to Model Checking. | Michael Leuschel, Stefan Gruner |
| 2001 | PADL | Design and Implementation of the High-Level Specification Language CSP(LP) in Prolog. | Michael Leuschel |
| 2000 | LPAR | Solving Planning Problems by Partial Deduction. | Helko Lehmann, Michael Leuschel |
| 2000 | PPDP | Solving coverability problems of petri nets by partial deduction. | Michael Leuschel, Helko Lehmann |
| 1999 | LOPSTR | Infinite State Model Checking by Abstract Interpretation and Program Specialisation. | Michael Leuschel, Thierry Massart |
| 1998 | ESOP | A Polyvariant Binding-Time Analysis for Off-line Partial Deduction. | Maurice Bruynooghe, Michael Leuschel, Konstantinos Sagonas |
| 1998 | ICLP | Program Specialisation and Abstract Interpretation Reconciled. | Michael Leuschel |
| 1998 | LOPSTR | Improving Homeomorphic Embedding for Online Termination. | Michael Leuschel |
| 1998 | PEPM | Logic Program Specialisation. | Michael Leuschel |
| 1998 | PEPM | Advanced Logic Program Specialisation. | Michael Leuschel |
| 1998 | SAS | On the Power of Homeomorphic Embedding for Online Termination. | Michael Leuschel |
| 1997 | LOPSTR | Termination Analysis for Tabled Logic Programming. | Stefaan Decorte, Danny De Schreye, Michael Leuschel, Bern Martens, Konstantinos Sagonas |
| 1997 | LOPSTR | Preserving Termination of Tabled Logic Programs While Unfolding. | Michael Leuschel, Bern Martens, Konstantinos Sagonas |
| 1996 | ICLP | A Conceptual Embedding of Folding into Partial Deduction: Towards a Maximal Integration. | Michael Leuschel, Danny De Schreye, D. Andre de Waal |
| 1996 | LOPSTR | Conjunctive Partial Deduction in Practice. | Jesper Jrgensen, Michael Leuschel, Bern Martens |
| 1996 | LOPSTR | Logic Program Specialisation: How to Be More Specific (Abstract). | Michael Leuschel, Danny De Schreye |
| 1996 | LOPSTR | Redundant Argument Filtering of Logic Programs. | Michael Leuschel, Morten Heine Srensen |
| 1995 | LOPSTR | Ecological Partial Deduction: Preserving Characteristic Trees Without Constraints. | Michael Leuschel |
| 1995 | PEPM | Towards Creating Specialised Integrity Checks through Partial Evaluation of Meta-Interpreters. | Michael Leuschel, Danny De Schreye |
| 1994 | LOPSTR | Partial Evaluation of the "Real Thing". | Michael Leuschel |