Partial Evaluation of the "Real Thing". - Michael Leuschel (LOPSTR, 1994)

Generating Specialised Update Procedures Through Partial Deduction of the Ground Representation. - Michael Leuschel; Bern Martens (Deductive Databases / Abduction in Deductive Databases, 1995)

Ecological Partial Deduction: Preserving Characteristic Trees Without Constraints. - Michael Leuschel (LOPSTR, 1995)

Towards Creating Specialised Integrity Checks through Partial Evaluation of Meta-Interpreters. - Michael Leuschel; Danny De Schreye (PEPM, 1995)

Partial Deduction of the Ground Representation and its Application to Integrity Checking. - Michael Leuschel; Bern Martens (ILPS, 1995)

Tutorial on Program Specialisation (Abstract). - Danny De Schreye; Michael Leuschel; Bern Martens (ILPS, 1995)

Efficiently Generating Efficient Generating Extensions in Prolog. - Jesper Jørgensen; Michael Leuschel (Dagstuhl Seminar on Partial Evaluation, 1996)

Global Control for Partial Deduction through Characteristic Atoms and Global Trees. - Michael Leuschel; Bern Martens (Dagstuhl Seminar on Partial Evaluation, 1996)

A Conceptual Embedding of Folding into Partial Deduction: Towards a Maximal Integration. - Michael Leuschel; Danny De Schreye; D. Andre de Waal (JICSLP, 1996)

Conjunctive Partial Deduction in Practice. - Jesper Jørgensen; Michael Leuschel; Bern Martens (LOPSTR, 1996)

Logic Program Specialisation: How to Be More Specific (Abstract). - Michael Leuschel; Danny De Schreye (LOPSTR, 1996)

Redundant Argument Filtering of Logic Programs. - Michael Leuschel; Morten Heine Sørensen (LOPSTR, 1996)

Logic Program Specialisation: How To Be More Specific. - Michael Leuschel; Danny De Schreye (PLILP, 1996)

Termination Analysis for Tabled Logic Programming. - Stefaan Decorte; Danny De Schreye; Michael Leuschel; Bern Martens; Konstantinos Sagonas (LOPSTR, 1997)

Preserving Termination of Tabled Logic Programs While Unfolding. - Michael Leuschel; Bern Martens; Konstantinos Sagonas (LOPSTR, 1997)

Specialization of Declarative Programs and Its Applications (Workshop Overview). - Michael Leuschel (ILPS, 1997)

Extending Homeomorphic Embedding in the Context of Logic Programming. - Michael Leuschel (WLP, 1997)

Constrained Partial Deduction. - Michael Leuschel; Danny De Schreye (WLP, 1997)

Advanced Techniques for Logic Program Specialisation. - Michael Leuschel (AI Commun., 1997)

A Polyvariant Binding-Time Analysis for Off-line Partial Deduction. - Maurice Bruynooghe; Michael Leuschel; Konstantinos Sagonas (ESOP, 1998)

Program Specialisation and Abstract Interpretation Reconciled. - Michael Leuschel (IJCSLP, 1998)

Improving Homeomorphic Embedding for Online Termination. - Michael Leuschel (LOPSTR, 1998)

Logic Program Specialisation. - Michael Leuschel (Partial Evaluation, 1998)

Advanced Logic Program Specialisation. - Michael Leuschel (Partial Evaluation, 1998)

On the Power of Homeomorphic Embedding for Online Termination. - Michael Leuschel (SAS, 1998)

Some Achievements and Prospects in Partial Deduction. - Michael Leuschel; Bern Martens; Danny De Schreye (ACM Comput. Surv., 1998)

Extending Partial Deduction to Tabled Execution: Some Results and Open Issues. - Konstantinos Sagonas; Michael Leuschel (ACM Comput. Surv., 1998)

Creating Specialised Integrity Checks Through Partial Evaluation of Meta-Interpreters. - Michael Leuschel; Danny De Schreye (J. Log. Program., 1998)

Constrained Partial Deduction and the Preservation of Characteristic Trees. - Michael Leuschel; Danny De Schreye (New Gener. Comput., 1998)

Controlling Generalization amd Polyvariance in Partial Deduction of Normal Logic Programs. - Michael Leuschel; Bern Martens; Danny De Schreye (ACM Trans. Program. Lang. Syst., 1998)

Abstraction-Based Partial Deduction for Solving Inverse Problems - A Transformational Approach to Software Verification. - Robert Glück; Michael Leuschel (Ershov Memorial Conference, 1999)

Sonic Partial Deduction. - Jonathan C. Martin; Michael Leuschel (Ershov Memorial Conference, 1999)

Infinite State Model Checking by Abstract Interpretation and Program Specialisation. - Michael Leuschel; Thierry Massart (LOPSTR, 1999)

Conjunctive Partial Deduction: Foundations, Control, Algorithms, and Experiments. - Danny De Schreye; Robert Glück; Jesper Jørgensen; Michael Leuschel; Bern Martens; Morten Heine Sørensen (J. Log. Program., 1999)

Preface - Workshop on Optimization and Implementation of Declarative Programs. - Michael Leuschel (WOID@ICLP, 1999)

Efficient Specialisation in Prolog Using the Hand-Written Compiler Generator LOGEN. - Michael Leuschel; Jesper Jørgensen (WOID@ICLP, 1999)

Decidability Results for the Propositional Fluent Calculus. - Helko Lehmann; Michael Leuschel (Computational Logic, 2000)

Coverability of Reset Petri Nets and Other Well-Structured Transition Systems by Partial Deduction. - Michael Leuschel; Helko Lehmann (Computational Logic, 2000)

Solving Planning Problems by Partial Deduction. - Helko Lehmann; Michael Leuschel (LPAR, 2000)

Solving coverability problems of petri nets by partial deduction. - Michael Leuschel; Helko Lehmann (PPDP, 2000)

Erratum to: "Conjunctive Partial Deduction: Foundations, Control, Algorithms and Experiments". - Danny De Schreye; Robert Glück; Jesper Jørgensen; Michael Leuschel; Bern Martens; Morten Heine Sørensen (J. Log. Program., 2000)

How to Make FDR Spin LTL Model Checking of CSP by Refinement. - Michael Leuschel; Thierry Massart; Andrew Currie (FME, 2001)

Abstract Conjunctive Partial Deduction Using Regular Types and Its Application to Model Checking. - Michael Leuschel; Stefan Gruner (LOPSTR, 2001)

Design and Implementation of the High-Level Specification Language CSP(LP) in Prolog. - Michael Leuschel (PADL, 2001)

Homeomorphic Embedding for Online Termination of Symbolic Methods. - Michael Leuschel (The Essence of Computation, 2002)

Book Reviews. - Michael Leuschel (Softw. Test. Verification Reliab., 2002)

Logic program specialisation through partial deduction: Control issues. - Michael Leuschel; Maurice Bruynooghe (Theory Pract. Log. Program., 2002)

The Benefits of Rapid Modelling for E-business System Development. - Juan Carlos Augusto; Carla Ferreira 001; Andrew M. Gravell; Michael Leuschel; Karen M. Y. Ng (ER (Workshops), 2003)

A Compiler Generator for Constraint Logic Programs. - Stephen-John Craig; Michael Leuschel (Ershov Memorial Conference, 2003)

ProB: A Model Checker for B. - Michael Leuschel; Michael J. Butler (FME, 2003)

Partial Evaluation of MATLAB. - Daniel Elphick; Michael Leuschel; Simon J. Cox 001 (GPCE, 2003)

Inductive Theorem Proving by Program Specialisation: Generating Proofs for Isabelle Using Ecce. - Helko Lehmann; Michael Leuschel (LOPSTR, 2003)

Model-Based Approaches for Validating Business Critical Systems. - Juan Carlos Augusto; Yvonne Howard; Andrew M. Gravell; Carla Ferreira 001; Stefan Gruner; Michael Leuschel (STEP, 2003)

A Trust Analysis Methodology for Pervasive Computing Systems. - Stéphane Lo Presti; Michael J. Butler; Michael Leuschel; Chris Booth (Trusting Agents for Trusting Electronic Societies, 2004)

LIX: an Effective Self-applicable Partial Evaluator for Prolog. - Stephen-John Craig; Michael Leuschel (FLOPS, 2004)

The Use of Formal Methods in the Analysis of Trust (Position Paper). - Michael J. Butler; Michael Leuschel; Stéphane Lo Presti; Phillip Turner (iTrust, 2004)

PROB: un outil de modélisation formelle. - Michael Leuschel (JFPLC, 2004)

Fully Automatic Binding-Time Analysis for Prolog. - Stephen-John Craig; John P. Gallagher; Michael Leuschel; Kim S. Henriksen (LOPSTR, 2004)

Specialising Interpreters Using Offline Partial Deduction. - Michael Leuschel; Stephen-John Craig; Maurice Bruynooghe; Wim Vanhoof (Program Development in Computational Logic, 2004)

Binding-Time Analysis for Mercury. - Wim Vanhoof; Maurice Bruynooghe; Michael Leuschel (Program Development in Computational Logic, 2004)

Efficient and flexible access control via logic program specialisation. - Steve Barker; Michael Leuschel; Mauricio Varea (PEPM, 2004)

Model checking object petri nets in prolog. - Berndt Farwer; Michael Leuschel (PPDP, 2004)

ProTest: An Automatic Test Environment for B Specifications. - Manoranjan Satpathy; Michael Leuschel; Michael J. Butler (MBT, 2004)

A framework for the integration of partial evaluation and abstract interpretation of logic programs. - Michael Leuschel (ACM Trans. Program. Lang. Syst., 2004)

Offline specialisation in Prolog using a hand-written compiler generator. - Michael Leuschel; Jesper Jørgensen; Wim Vanhoof; Maurice Bruynooghe (Theory Pract. Log. Program., 2004)

Introduction to the Special Issue on Verification and Computational Logic. - Michael Leuschel; Andreas Podelski; C. R. Ramakrishnan 001; Ulrich Ultes-Nitsche (Theory Pract. Log. Program., 2004)

Tools for System Validation with B Abstract Machines. - Michael J. Butler; Michael Leuschel; Colin F. Snook (Abstract State Machines, 2005)

Forward Slicing by Conjunctive Partial Deduction and Argument Filtering. - Michael Leuschel; Germán Vidal (ESOP, 2005)

Combining CSP and B for Specification and Property Verification. - Michael J. Butler; Michael Leuschel (FM, 2005)

Automatic Refinement Checking for B. - Michael Leuschel; Michael J. Butler (ICFEM, 2005)

Towards Provably Correct Code Generation via Horn Logical Continuation Semantics. - Qian Wang 024; Gopal Gupta 001; Michael Leuschel (PADL, 2005)

Self-tuning resource aware specialisation for prolog. - Stephen-John Craig; Michael Leuschel (PPDP, 2005)

Visualising Larger State Spaces in Pro B. - Michael Leuschel; Edd Turner (ZB, 2005)

Guest Editorial. - Michael Leuschel (Formal Aspects Comput., 2005)

Supervising Offline Partial Evaluation of Logic Programs Using Online Techniques. - Michael Leuschel; Stephen-John Craig; Daniel Elphick (LOPSTR, 2006)

The Ecce and Logen partial evaluators and their web interfaces. - Michael Leuschel; Daniel Elphick; Mauricio Varea; Stephen-John Craig; Marc Fontaine (PEPM, 2006)

Rapid Visualization of B Specifications containing Higher-Order Recursive Functions. - Jens Bendisposto; Michael Leuschel (Softwaretechnik-Trends, 2006)

Efficient Approximate Verification of Promela Models Via Symmetry Markers. - Dragan Bosnacki; Alastair F. Donaldson; Michael Leuschel; Thierry Massart (ATVA, 2007)

A Generic Flash-Based Animation Engine for ProB. - Jens Bendisposto; Michael Leuschel (B, 2007)

BE4: The B Extensible Eclipse Editing Environment. - Jens Bendisposto; Michael Leuschel (B, 2007)

Symmetry Reduction for B by Permutation Flooding. - Michael Leuschel; Michael J. Butler; Corinna Spermann; Edd Turner (B, 2007)

Animating and Model Checking B Specifications with Higher-Order Recursive Functions. - Michael Leuschel; Jens Bendisposto (Rigorous Methods for Software Construction and Analysis, 2007)

Validating Z Specifications Using the ProBAnimator and Model Checker. - Daniel Plagge; Michael Leuschel (IFM, 2007)

Partial Evaluation of Pointcuts. - Karl Klose; Klaus Ostermann; Michael Leuschel (PADL, 2007)

Automatic Testing from Formal Specifications. - Manoranjan Satpathy; Michael J. Butler; Michael Leuschel; S. Ramesh 002 (TAP, 2007)

Symmetry Reduced Model Checking for B. - Edd Turner; Michael Leuschel; Corinna Spermann; Michael J. Butler (TASE, 2007)

The High Road to Formal Validation: . - Michael Leuschel (ABZ, 2008)

Towards Demonstrably Correct Compilation of Java Byte Code. - Michael Leuschel (FMCO, 2008)

Probing the Depths of CSP-M: A New fdr-Compliant Validation Tool. - Michael Leuschel; Marc Fontaine (ICFEM, 2008)

The MEB and CEB Static Analysis for CSP Specifications. - Michael Leuschel; Marisa Llorens; Javier Oliver 001; Josep Silva; Salvador Tamarit (LOPSTR, 2008)

Fast Offline Partial Evaluation of Large Logic Programs. - Michael Leuschel; Germán Vidal (LOPSTR, 2008)

Declarative programming for verification: lessons and outlook. - Michael Leuschel (PPDP, 2008)

ProB gets Nauty: Effective Symmetry Reduction for B and Z Models. - Corinna Spermann; Michael Leuschel (TASE, 2008)

Efficient and flexible access control via Jones-optimal logic program specialisation. - Steve Barker; Michael Leuschel; Mauricio Varea (High. Order Symb. Comput., 2008)

Editorial. - Julia Lawall; Michael Leuschel; Peter Sestoft (High. Order Symb. Comput., 2008)

ProB: an automated analysis toolset for the B method. - Michael Leuschel; Michael J. Butler (Int. J. Softw. Tools Technol. Transf., 2008)

La validation de modèles Event-B avec le plug-in ProB pour RODIN. - Jens Bendisposto; Michael Leuschel; O. Ligot; Mireille Samia (Tech. Sci. Informatiques, 2008)

Validating and Animating Higher-Order Recursive Functions in B. - Michael Leuschel; Dominique Cansell; Michael J. Butler (Rigorous Methods for Software Construction and Analysis, 2009)

Automated Property Verification for Large Scale B Models. - Michael Leuschel; Jérôme Falampin; Fabian Fritz; Daniel Plagge (FM, 2009)

Visualising Event-B Models with B-Motion Studio. - Lukas Ladenberger; Jens Bendisposto; Michael Leuschel (FMICS, 2009)

Proof Assisted Model Checking for B. - Jens Bendisposto; Michael Leuschel (ICFEM, 2009)

Towards pie tree visualization of graphs and large software architectures. - Mireille Samia; Michael Leuschel (ICPC, 2009)

Towards Just-In-Time Partial Evaluation of Prolog. - Carl Friedrich Bolz; Michael Leuschel; Armin Rigo (LOPSTR, 2009)

SOC: a slicer for CSP specifications. - Michael Leuschel; Marisa Llorens; Javier Oliver 001; Josep Silva; Salvador Tamarit (PEPM, 2009)

Applying Model Checking to Generate Model-Based Integration Tests from Choreography Models. - Sebastian Wieczorek; Vitaly Kozyura; Andreas Roth 001; Michael Leuschel; Jens Bendisposto; Daniel Plagge; Ina Schieferdecker (TestCom/FATES, 2009)

Pie Tree Visualization. - Mireille Samia; Michael Leuschel (SEKE, 2009)

How to Explain Mistakes. - Stefan Hallerstede; Michael Leuschel (TFM, 2009)

Fast and Accurate Strong Termination Analysis with an Application to Partial Evaluation. - Michael Leuschel; Salvador Tamarit; Germán Vidal (WFLP, 2009)

Improving Size-Change Analysis in Offline Partial Evaluation - Michael Leuschel; Salvador Tamarit; Germán Vidal (CoRR, 2009)

A Semantics-Aware Editing Environment for Prolog in Eclipse - Jens Bendisposto; Ian Endrijautzki; Michael Leuschel; David Schneider 001 (CoRR, 2009)

Refinement-Animation for Event-B - Towards a Method of Validation. - Stefan Hallerstede; Michael Leuschel; Daniel Plagge (ASM, 2010)

A Refinement-Based Correctness Proof of Symmetry Reduced Model Checking. - Edd Turner; Michael J. Butler; Michael Leuschel (ASM, 2010)

Towards a jitting VM for prolog execution. - Carl Friedrich Bolz; Michael Leuschel; David Schneider 001 (PPDP, 2010)

Directed Model Checking for B: An Evaluation and New Techniques. - Michael Leuschel; Jens Bendisposto (SBMF, 2010)

An Approach of Requirements Tracing in Formal Refinement. - Michael Jastram; Stefan Hallerstede; Michael Leuschel; Aryldo G. Russo (VSTTE, 2010)

Efficient approximate verification of B and Z models via symmetry markers. - Michael Leuschel; Thierry Massart (Ann. Math. Artif. Intell., 2010)

Avocs2010 Preface. - Jens Bendisposto; Michael Leuschel; Markus Roggenbach (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2010)

Seven at one stroke: LTL model checking for high-level specifications in B, Z, CSP, and more. - Daniel Plagge; Michael Leuschel (Int. J. Softw. Tools Technol. Transf., 2010)

Runtime feedback in a meta-tracing JIT for efficient dynamic languages. - Carl Friedrich Bolz; Antonio Cuni; Maciej Fijalkowski; Michael Leuschel; Samuele Pedroni; Armin Rigo (ICOOOLPS@ECOOP, 2011)

Automatic Flow Analysis for Event-B. - Jens Bendisposto; Michael Leuschel (FASE, 2011)

On Fitting a Formal Method into Practice. - Rainer Gmehlich; Katrin Grau; Stefan Hallerstede; Michael Leuschel; Felix Lösch; Daniel Plagge (ICFEM, 2011)

Allocation removal by partial evaluation in a tracing JIT. - Carl Friedrich Bolz; Antonio Cuni; Maciej Fijalkowski; Michael Leuschel; Samuele Pedroni; Armin Rigo (PEPM, 2011)

Preface. - Alexander B. Romanovsky; Cliff B. Jones; Jens Bendisposto; Michael Leuschel (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2011)

Automated property verification for large scale B models with ProB. - Michael Leuschel; Jérôme Falampin; Fabian Fritz; Daniel Plagge (Formal Aspects Comput., 2011)

Selected papers on Integrated Formal Methods (iFM09). - Michael Leuschel; Heike Wehrheim (Sci. Comput. Program., 2011)

Developing Camille, a text editor for Rodin. - Jens Bendisposto; Fabian Fritz; Michael Jastram; Michael Leuschel; Ingo Weigelt (Softw. Pract. Exp., 2011)

Constraint-based deadlock checking of high-level specifications. - Stefan Hallerstede; Michael Leuschel (Theory Pract. Log. Program., 2011)

Validating B, Z and TLA + Using ProB and Kodkod. - Daniel Plagge; Michael Leuschel (FM, 2012)

Translating TLA + to B for Validation with ProB. - Dominik Hansen; Michael Leuschel (IFM, 2012)

Formally Checking Large Data Sets in the Railways - Thierry Lecomte; Lilian Burdy; Michael Leuschel (CoRR, 2012)

Experiments in program verification using Event-B. - Stefan Hallerstede; Michael Leuschel (Formal Aspects Comput., 2012)

Static slicing of explicitly synchronized languages. - Michael Leuschel; Marisa Llorens; Javier Oliver 001; Josep Silva; Salvador Tamarit (Inf. Comput., 2012)

Improving Railway Data Validation with ProB. - Jérôme Falampin; Hung Le-Dang; Michael Leuschel; Mikael Mokrani; Daniel Plagge (Industrial Deployment of System Engineering Methods, 2013)

Inferring Physical Units in B Models. - Sebastian Krings; Michael Leuschel (SEFM, 2013)

Integration of Tools for Rigorous Software Construction and Analysis (Dagstuhl Seminar 13372). - Uwe Glässer; Stefan Hallerstede; Michael Leuschel; Elvinia Riccobene (Dagstuhl Reports, 2013)

Validation of formal models by refinement animation. - Stefan Hallerstede; Michael Leuschel; Daniel Plagge (Sci. Comput. Program., 2013)

Translating B to TLA + for Validation with TLC. - Dominik Hansen; Michael Leuschel (ABZ, 2014)

Towards B as a High-Level Constraint Modelling Language - Solving the Jobs Puzzle Challenge. - Michael Leuschel; David Schneider 001 (ABZ, 2014)

Towards Constraint-Solving over Higher-Order Unbounded Datatypes using Formal Methods Tools. - Michael Leuschel (VPT@CAV, 2014)

An Approach for Creating Domain Specific Visualisations of CSP Models. - Lukas Ladenberger; Ivaylo Dobrikov; Michael Leuschel (SEFM Workshops, 2014)

Who watches the watchers: Validating the ProB Validation Tool. - Jens Bendisposto; Sebastian Krings; Michael Leuschel (F-IDE, 2014)

Checking Computations of Formal Method Tools - A Secondary Toolchain for ProB. - John Witulski; Michael Leuschel (F-IDE, 2014)

Fast offline partial evaluation of logic programs. - Michael Leuschel; Germán Vidal (Inf. Comput., 2014)

Preface of Automated Verification of Critical Systems 2010 (AVoCS 2010). - Jens Bendisposto; Michael Leuschel; Markus Roggenbach (Sci. Comput. Program., 2014)

Introduction to the 30th International Conference on Logic Programming Special Issue. - Michael Leuschel; Tom Schrijvers (Theory Pract. Log. Program., 2014)

Mastering the Visualization of Larger State Spaces with Projection Diagrams. - Lukas Ladenberger; Michael Leuschel (ICFEM, 2015)

From Failure to Proof: The ProB Disprover for B and Event-B. - Sebastian Krings; Jens Bendisposto; Michael Leuschel (SEFM, 2015)

Model-Based Robustness Testing in Event-B Using Mutation. - Aymerick Savary; Marc Frappier; Michael Leuschel; Jean-Louis Lanet (SEFM, 2015)

Generating Event-B Specifications from Algorithm Descriptions. - Joy Clark; Jens Bendisposto; Stefan Hallerstede; Dominik Hansen; Michael Leuschel (ABZ, 2016)

Using B and ProB for Data Validation Projects. - Dominik Hansen; David Schneider 001; Michael Leuschel (ABZ, 2016)

Proof Assisted Symbolic Model Checking for B and Event-B. - Sebastian Krings; Michael Leuschel (ABZ, 2016)

A Compact Encoding of Sequential ASMs in Event-B. - Michael Leuschel; Egon Börger (ABZ, 2016)

Interactive Model Repair by Synthesis. - Joshua Schmidt; Sebastian Krings; Michael Leuschel (ABZ, 2016)

Symbolic Reachability Analysis of B Through ProB and LTSmin. - Jens Bendisposto; Philipp Körner; Michael Leuschel; Jeroen Meijer; Jaco van de Pol; Helen Treharne; Jorden Whitefield (IFM, 2016)

SMT Solvers for Validation of B and Event-B Models. - Sebastian Krings; Michael Leuschel (IFM, 2016)

Formal Model-Based Constraint Solving and Document Generation. - Michael Leuschel (SBMF, 2016)

LTL Model Checking under Fairness in ProB. - Ivaylo Dobrikov; Michael Leuschel; Daniel Plagge (SEFM, 2016)

BMotionWeb: A Tool for Rapid Creation of Formal Prototypes. - Lukas Ladenberger; Michael Leuschel (SEFM, 2016)

Knowledge Representation Analysis of Graph Mining. - Matthias van der Hallen; Sergey Paramonov 001; Michael Leuschel; Gerda Janssens (CoRR, 2016)

Optimising the ProB model checker for B using partial order reduction. - Ivaylo Dobrikov; Michael Leuschel (Formal Aspects Comput., 2016)

Translating B to TLA+ for validation with TLC. - Dominik Hansen; Michael Leuschel (Sci. Comput. Program., 2016)

Constraint Logic Programming over Infinite Domains with an Application to Proof. - Sebastian Krings; Michael Leuschel (WLP / WFLP, 2017)

Inferring physical units in formal models. - Sebastian Krings; Michael Leuschel (Softw. Syst. Model., 2017)

Validation of the ABZ landing gear system using ProB. - Lukas Ladenberger; Dominik Hansen; Harald Wiegard; Jens Bendisposto; Michael Leuschel (Int. J. Softw. Tools Technol. Transf., 2017)

Using a Formal B Model at Runtime in a Demonstration of the ETCS Hybrid Level 3 Concept with Real Trains. - Dominik Hansen; Michael Leuschel; David Schneider 001; Sebastian Krings; Philipp Körner; Thomas Naulin; Nader Nayeri; Frank Skowron (ABZ, 2018)

A Translation from Alloy to B. - Sebastian Krings; Joshua Schmidt; Carola Brings; Marc Frappier; Michael Leuschel (ABZ, 2018)

Extended Algebraic State-Transition Diagrams. - Lionel N. Tidjon; Marc Frappier; Michael Leuschel; Amel Mammar (ICECCS, 2018)

Formalisation of SysML/KAOS Goal Assignments with B System Component Decompositions. - Steve Jeffrey Tueno Fotso; Marc Frappier; Régine Laleau; Amel Mammar; Michael Leuschel (IFM, 2018)

State-of-the-Art Model Checking for B and Event-B Using ProB and LTSmin. - Philipp Körner; Michael Leuschel; Jeroen Meijer (IFM, 2018)

Repair and Generation of Formal Models Using Synthesis. - Joshua Schmidt; Sebastian Krings; Michael Leuschel (IFM, 2018)

Three Is a Crowd: SAT, SMT and CLP on a Chessboard. - Sebastian Krings; Michael Leuschel; Philipp Körner; Stefan Hallerstede; Miran Hasanagic (PADL, 2018)

From Software Specifications to Constraint Programming. - Stefan Hallerstede; Miran Hasanagic; Sebastian Krings; Peter Gorm Larsen; Michael Leuschel (SEFM, 2018)

Solving Set Constraints in B and Event-B: Foundations and Applications (invited talk). - Michael Leuschel (SETS@ABZ, 2018)

Model-based problem solving for university timetable validation and improvement. - David Schneider 001; Michael Leuschel; Tobias Witt (Formal Aspects Comput., 2018)

Enabling analysis for Event-B. - Ivaylo Dobrikov; Michael Leuschel (Sci. Comput. Program., 2018)

Proof assisted bounded and unbounded symbolic model checking of software and system models. - Sebastian Krings; Michael Leuschel (Sci. Comput. Program., 2018)

Embedding High-Level Formal Specifications into Applications. - Philipp Körner; Jens Bendisposto; Jannik Dunkelau; Sebastian Krings; Michael Leuschel (FM, 2019)

Embedding SMT-LIB into B for Interactive Proof and Constraint Solving. - Sebastian Krings; Michael Leuschel (IFM, 2019)

A Multi-target Code Generator for High-Level B. - Fabian Vu; Dominik Hansen; Philipp Körner; Michael Leuschel (IFM, 2019)

Property-Based Modelling and Validation of a CBTC Zone Controller in Event-B. - Mathieu Comptier; Michael Leuschel; Luis-Fernando Mejia; Julien Molinero Perez; Mareike Mutz (RSSRail, 2019)

Applying Formal Reasoning to Model Transformation: The Meeduse solution. - Akram Idani; Germán Vega; Michael Leuschel (TTC@STAF, 2019)

Software Architecture of Modern Model Checkers. - Fabrice Kordon; Michael Leuschel; Jaco van de Pol; Yann Thierry-Mieg (Computing and Software Science, 2019)

Analysing ProB's Constraint Solving Backends - What Do They Know? Do They Know Things? Let's Find Out! - Jannik Dunkelau; Joshua Schmidt; Michael Leuschel (ABZ, 2020)

ProB and Jupyter for Logic, Set Theory, Theoretical Computer Science and Formal Methods. - David Geleßus; Michael Leuschel (ABZ, 2020)

Towards a Shared Specification Repository. - Philipp Körner; Michael Leuschel; Jannik Dunkelau (ABZ, 2020)

Modelling and Validating an Automotive System in Classical B and Event-B. - Michael Leuschel; Mareike Mutz; Michelle Werth (ABZ, 2020)

VisB: A Lightweight Tool to Visualize Formal Models with SVG Graphics. - Michelle Werth; Michael Leuschel (ABZ, 2020)

The First Twenty-Five Years of Industrial Use of the B-Method. - Michael J. Butler; Philipp Körner; Sebastian Krings; Thierry Lecomte; Michael Leuschel; Luis-Fernando Mejia; Laurent Voisin (FMICS, 2020)

Fast and Effective Well-Definedness Checking. - Michael Leuschel (IFM, 2020)

On the Performance of Bytecode Interpreters in Prolog. - Philipp Körner; David Schneider 001; Michael Leuschel (WFLP, 2020)

Prolog for Verification, Analysis and Transformation Tools. - Michael Leuschel (VPT/HCVS@ETAPS, 2020)

Translating Alloy and extensions to classical B. - Sebastian Krings; Michael Leuschel; Joshua Schmidt; David Schneider 001; Marc Frappier (Sci. Comput. Program., 2020)

Validation and real-life demonstration of ETCS hybrid level 3 principles using a formal B model. - Dominik Hansen; Michael Leuschel; Philipp Körner; Sebastian Krings; Thomas Naulin; Nader Nayeri; David Schneider 001; Frank Skowron (Int. J. Softw. Tools Technol. Transf., 2020)

Validation of Formal Models by Timed Probabilistic Simulation. - Fabian Vu; Michael Leuschel; Atif Mashkoor (ABZ, 2021)

Spot the Difference: A Detailed Comparison Between B and Event-B. - Michael Leuschel (Logic, Computation and Rigorous Methods, 2021)

ProB2-UI: A Java-Based User Interface for ProB. - Jens Bendisposto; David Geleßus; Yumiko Jansing; Michael Leuschel; Antonia Pütz; Fabian Vu; Michelle Werth (FMICS, 2021)

Improving SMT Solver Integrations for the Validation of B and Event-B Models. - Joshua Schmidt; Michael Leuschel (FMICS, 2021)

Validation Obligations: A Novel Approach to Check Compliance between Requirements and their Formal Specification. - Atif Mashkoor; Michael Leuschel; Alexander Egyed (ICSE (NIER), 2021)

Integrating formal specifications into applications: the ProB Java API. - Philipp Körner; Jens Bendisposto; Jannik Dunkelau; Sebastian Krings; Michael Leuschel (Formal Methods Syst. Des., 2021)

Generating Domain-Specific Interactive Validation Documents. - Fabian Vu; Christopher Happe; Michael Leuschel (FMICS, 2022)

Trace Refinement in B and Event-B. - Sebastian Stock 002; Atif Mashkoor; Michael Leuschel; Alexander Egyed (ICFEM, 2022)

Model Checking B Models via High-Level Code Generation. - Fabian Vu; Dominik Brandt; Michael Leuschel (ICFEM, 2022)

Operation Caching and State Compression for Model Checking of High-Level Models - How to Have Your Cake and Eat It. - Michael Leuschel (IFM, 2022)

Towards Practical Partial Order Reduction for High-Level Formalisms. - Philipp Körner; Michael Leuschel (VSTTE, 2022)

50 Years of Prolog and Beyond. - Philipp Körner; Michael Leuschel; João Barbosa; Vítor Santos Costa; Verónica Dahl; Manuel V. Hermenegildo; José F. Morales 001; Jan Wielemaker; Daniel Diaz 001; Salvador Abreu; Giovanni Ciatto (CoRR, 2022)

IVOIRE Deliverable 1.1: Classification of existing VOs & tools and Formalization of VOs semantics. - Sebastian Stock 002; Fabian Vu; Atif Mashkoor; Michael Leuschel; Alexander Egyed (CoRR, 2022)

Formalization of Advanced VOs semantics and VO Refinement. - Sebastian Stock 002; Fabian Vu; David Geleßus; Atif Mashkoor; Michael Leuschel; Alexander Egyed (CoRR, 2022)

SMT solving for the validation of B and Event-B models. - Joshua Schmidt; Michael Leuschel (Int. J. Softw. Tools Technol. Transf., 2022)

Making ProB Compatible with SWI-Prolog. - David Geleßus; Michael Leuschel (Theory Pract. Log. Program., 2022)

Fifty Years of Prolog and Beyond. - Philipp Körner; Michael Leuschel; João Barbosa; Vítor Santos Costa; Verónica Dahl; Manuel V. Hermenegildo; José F. Morales 001; Jan Wielemaker; Daniel Diaz 001; Salvador Abreu (Theory Pract. Log. Program., 2022)

ProB Operation Caching ifm2022 Artefact. - Michael Leuschel (Zenodo, 2022)

ProB Linux 1.12.0-beta1. - Michael Leuschel (Zenodo, 2022)

ProB Operation Caching ifm2022 Artefact. - Michael Leuschel (Zenodo, 2022)

Performance Fuzzing with Reinforcement-Learning and Well-Defined Constraints for the B Method. - Jannik Dunkelau; Michael Leuschel (iFM, 2023)

A Formal Model of Train Control with AI-Based Obstacle Detection. - Jan Gruteser; David Geleßus; Michael Leuschel; Jan Roßbach; Fabian Vu (RSSRail, 2023)

Modelling, Visualisation and Proof of an ETCS Level 3 Moving Block System. - Michael Leuschel; Nader Nayeri (RSSRail, 2023)

Modeling and Analysis of a Safety-Critical Interactive System Through Validation Obligations. - David Geleßus; Sebastian Stock 002; Fabian Vu; Michael Leuschel; Atif Mashkoor (ABZ, 2023)

Modeling and Verifying an Arrival Manager Using Event-B. - Amel Mammar; Michael Leuschel (ABZ, 2023)

Validation by Abstraction and Refinement. - Sebastian Stock 002; Fabian Vu; David Geleßus; Michael Leuschel; Atif Mashkoor; Alexander Egyed (ABZ, 2023)

Validation of Formal Models by Interactive Simulation. - Fabian Vu; Michael Leuschel (ABZ, 2023)

Certified Control for Train Sign Classification. - Jan Roßbach; Michael Leuschel (FMAS@iFM, 2023)

ProB: Harnessing the Power of Prolog to Bring Formal Models and Mathematics to Life. - Michael Leuschel (Prolog: The Next 50 Years, 2023)

B2SAT: A Bare-Metal Reduction of B to SAT. - Michael Leuschel (FM (2), 2024)

Validation of RailML Using ProB. - Jan Gruteser; Michael Leuschel (ICECCS, 2024)

Evaluating AI-Based Components in Autonomous Railway Systems - A Methodology. - Jan Roßbach; Oliver De Candido; Ahmed Hammam; Michael Leuschel (KI, 2024)

Validation of Reinforcement Learning Agents and Safety Shields with ProB. - Fabian Vu; Jannik Dunkelau; Michael Leuschel (NFM, 2024)

Towards a Novel Approach to Railway Safety Using STPA and Promise Theory. - Felix Schaber; Atif Mashkoor; Michael Leuschel (SFPVV, 2024)

Using Formal Models, Safety Shields and Certified Control to Validate AI-Based Train Systems. - Jan Gruteser; Jan Roßbach; Fabian Vu; Michael Leuschel (FMAS@iFM, 2024)

Specifications are Preferably Amenable to Proof and Animation. - Michael Leuschel (The Practice of Formal Methods (I), 2024)

Trace preservation in B and Event-B refinements. - Sebastian Stock 002; Atif Mashkoor; Michael Leuschel; Alexander Egyed (J. Log. Algebraic Methods Program., 2024)

Generating interactive documents for domain-specific validation of formal models. - Fabian Vu; Christopher Happe; Michael Leuschel (Int. J. Softw. Tools Technol. Transf., 2024)

ProB Linux 1.13.1-beta. - Michael Leuschel (Zenodo, 2024)

ProB - B2SAT Artifact for FM'2024. - Michael Leuschel (Zenodo, 2024)

ProB - B2SAT Artifact for FM'2024. - Michael Leuschel (Zenodo, 2024)

ProB - B2SAT Artifact for FM'2024. - Michael Leuschel (Zenodo, 2024)

ProB - B2SAT Artifact for FM'2024. - Michael Leuschel (Zenodo, 2024)

Promise-Driven Modeling: A Structured Approach for Modeling Cyber-Physical Systems. - Felix Schaber; Atif Mashkoor; Michael Leuschel (FMICS, 2025)

Failure Divergence Refinement for Event-B. - Sebastian Stock 002; Michael Leuschel; Atif Mashkoor (TASE, 2025)

Case Study: Safety Controller for Autonomous Driving on Highways. - Michael Leuschel; Fabian Vu; Kristin Rutenkolk (ABZ, 2025)

Formal Methods in Industry. - 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 001; Cristina Seceleanu; et al. (Formal Aspects Comput., 2025)