Michael Leuschel

According to our database1, Michael Leuschel authored at least 175 papers between 1994 and 2019.

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepages:

On csauthors.net:

Bibliography

2019
Property-Based Modelling and Validation of a CBTC Zone Controller in Event-B.
Proceedings of the Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification, 2019

2018
Proof assisted bounded and unbounded symbolic model checking of software and system models.
Sci. Comput. Program., 2018

Solving Set Constraints in B and Event-B: Foundations and Applications (invited talk).
Proceedings of the 3rd International Workshop on Sets and Tools co-located with the 6th International ABZ Conference, 2018

From Software Specifications to Constraint Programming.
Proceedings of the Software Engineering and Formal Methods - 16th International Conference, 2018

Three Is a Crowd: SAT, SMT and CLP on a Chessboard.
Proceedings of the Practical Aspects of Declarative Languages, 2018

Repair and Generation of Formal Models Using Synthesis.
Proceedings of the Integrated Formal Methods - 14th International Conference, 2018

State-of-the-Art Model Checking for B and Event-B Using ProB and LTSmin.
Proceedings of the Integrated Formal Methods - 14th International Conference, 2018

Formalisation of SysML/KAOS Goal Assignments with B System Component Decompositions.
Proceedings of the Integrated Formal Methods - 14th International Conference, 2018

Extended Algebraic State-Transition Diagrams.
Proceedings of the 23rd International Conference on Engineering of Complex Computer Systems, 2018

A Translation from Alloy to B.
Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2018

Using a Formal B Model at Runtime in a Demonstration of the ETCS Hybrid Level 3 Concept with Real Trains.
Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2018

2017
Validation of the ABZ landing gear system using ProB.
STTT, 2017

Inferring physical units in formal models.
Software and System Modeling, 2017

Constraint Logic Programming over Infinite Domains with an Application to Proof.
Proceedings of the Proceedings 29th and 30th Workshops on (Constraint) Logic Programming and 24th International Workshop on Functional and (Constraint) Logic Programming, 2017

2016
Translating B to TLA+ for validation with TLC.
Sci. Comput. Program., 2016

BMotionWeb: A Tool for Rapid Creation of Formal Prototypes.
Proceedings of the Software Engineering and Formal Methods - 14th International Conference, 2016

LTL Model Checking under Fairness in ProB.
Proceedings of the Software Engineering and Formal Methods - 14th International Conference, 2016

Formal Model-Based Constraint Solving and Document Generation.
Proceedings of the Formal Methods: Foundations and Applications - 19th Brazilian Symposium, 2016

SMT Solvers for Validation of B and Event-B Models.
Proceedings of the Integrated Formal Methods - 12th International Conference, 2016

Symbolic Reachability Analysis of B Through ProB and LTSmin.
Proceedings of the Integrated Formal Methods - 12th International Conference, 2016

Interactive Model Repair by Synthesis.
Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2016

A Compact Encoding of Sequential ASMs in Event-B.
Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2016

Proof Assisted Symbolic Model Checking for B and Event-B.
Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2016

Using B and ProB for Data Validation Projects.
Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2016

Enabling Analysis for Event-B.
Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2016

Generating Event-B Specifications from Algorithm Descriptions.
Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2016

2015
Model-Based Robustness Testing in Event-B Using Mutation.
Proceedings of the Software Engineering and Formal Methods - 13th International Conference, 2015

From Failure to Proof: The ProB Disprover for B and Event-B.
Proceedings of the Software Engineering and Formal Methods - 13th International Conference, 2015

Mastering the Visualization of Larger State Spaces with Projection Diagrams.
Proceedings of the Formal Methods and Software Engineering, 2015

Model-Based Problem Solving for University Timetable Validation and Improvement.
Proceedings of the FM 2015: Formal Methods, 2015

2014
Introduction to the 30th International Conference on Logic Programming Special Issue.
TPLP, 2014

Preface of Automated Verification of Critical Systems 2010 (AVoCS 2010).
Sci. Comput. Program., 2014

Fast offline partial evaluation of logic programs.
Inf. Comput., 2014

Checking Computations of Formal Method Tools - A Secondary Toolchain for ProB.
Proceedings of the Proceedings 1st Workshop on Formal Integrated Development Environment, 2014

Who watches the watchers: Validating the ProB Validation Tool.
Proceedings of the Proceedings 1st Workshop on Formal Integrated Development Environment, 2014

An Approach for Creating Domain Specific Visualisations of CSP Models.
Proceedings of the Software Engineering and Formal Methods, 2014

Optimising the ProB Model Checker for B Using Partial Order Reduction.
Proceedings of the Software Engineering and Formal Methods - 12th International Conference, 2014

Towards Constraint-Solving over Higher-Order Unbounded Datatypes using Formal Methods Tools.
Proceedings of the VPT 2014. Second International Workshop on Verification and Program Transformation, 2014

Towards B as a High-Level Constraint Modelling Language - Solving the Jobs Puzzle Challenge.
Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2014

Validation of the ABZ Landing Gear System Using ProB.
Proceedings of the ABZ 2014: The Landing Gear Case Study, 2014

Translating B to TLA + for Validation with TLC.
Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2014

2013
Validation of formal models by refinement animation.
Sci. Comput. Program., 2013

Integration of Tools for Rigorous Software Construction and Analysis (Dagstuhl Seminar 13372).
Dagstuhl Reports, 2013

Inferring Physical Units in B Models.
Proceedings of the Software Engineering and Formal Methods - 11th International Conference, 2013

Improving Railway Data Validation with ProB.
Proceedings of the Industrial Deployment of System Engineering Methods, 2013

2012
Static slicing of explicitly synchronized languages.
Inf. Comput., 2012

Experiments in program verification using Event-B.
Formal Asp. Comput., 2012

Translating TLA + to B for Validation with ProB.
Proceedings of the Integrated Formal Methods - 9th International Conference, 2012

Validating B, Z and TLA + Using ProB and Kodkod.
Proceedings of the FM 2012: Formal Methods, 2012

2011
Constraint-based deadlock checking of high-level specifications.
TPLP, 2011

Developing Camille, a text editor for Rodin.
Softw., Pract. Exper., 2011

Selected papers on Integrated Formal Methods (iFM09).
Sci. Comput. Program., 2011

Automated property verification for large scale B models with ProB.
Formal Asp. Comput., 2011

Preface.
ECEASST, 2011

Allocation removal by partial evaluation in a tracing JIT.
Proceedings of the 2011 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, 2011

On Fitting a Formal Method into Practice.
Proceedings of the Formal Methods and Software Engineering, 2011

Automatic Flow Analysis for Event-B.
Proceedings of the Fundamental Approaches to Software Engineering, 2011

Runtime feedback in a meta-tracing JIT for efficient dynamic languages.
Proceedings of the 6th Workshop on Implementation, 2011

2010
Seven at one stroke: LTL model checking for high-level specifications in B, Z, CSP, and more.
STTT, 2010

Avocs2010 Preface.
ECEASST, 2010

Efficient approximate verification of B and Z models via symmetry markers.
Ann. Math. Artif. Intell., 2010

An Approach of Requirements Tracing in Formal Refinement.
Proceedings of the Verified Software: Theories, 2010

Directed Model Checking for B: An Evaluation and New Techniques.
Proceedings of the Formal Methods: Foundations and Applications, 2010

Towards a jitting VM for prolog execution.
Proceedings of the 12th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2010

A Refinement-Based Correctness Proof of Symmetry Reduced Model Checking.
Proceedings of the Abstract State Machines, 2010

Refinement-Animation for Event-B - Towards a Method of Validation.
Proceedings of the Abstract State Machines, 2010

2009
Fast and Accurate Strong Termination Analysis with an Application to Partial Evaluation.
Proceedings of the Functional and Constraint Logic Programming, 2009

How to Explain Mistakes.
Proceedings of the Teaching Formal Methods, Second International Conference, 2009

Pie Tree Visualization.
Proceedings of the 21st International Conference on Software Engineering & Knowledge Engineering (SEKE'2009), 2009

Applying Model Checking to Generate Model-Based Integration Tests from Choreography Models.
Proceedings of the Testing of Software and Communication Systems, 2009

SOC: a slicer for CSP specifications.
Proceedings of the 2009 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-based Program Manipulation, 2009

Towards Just-In-Time Partial Evaluation of Prolog.
Proceedings of the Logic-Based Program Synthesis and Transformation, 2009

Towards pie tree visualization of graphs and large software architectures.
Proceedings of the 17th IEEE International Conference on Program Comprehension, 2009

Proof Assisted Model Checking for B.
Proceedings of the Formal Methods and Software Engineering, 2009

Visualising Event-B Models with B-Motion Studio.
Proceedings of the Formal Methods for Industrial Critical Systems, 2009

Automated Property Verification for Large Scale B Models.
Proceedings of the FM 2009: Formal Methods, 2009

Validating and Animating Higher-Order Recursive Functions in B.
Proceedings of the Rigorous Methods for Software Construction and Analysis, 2009

2008
La validation de modèles Event-B avec le plug-in ProB pour RODIN.
Technique et Science Informatiques, 2008

ProB: an automated analysis toolset for the B method.
STTT, 2008

Editorial.
Higher-Order and Symbolic Computation, 2008

Efficient and flexible access control via Jones-optimal logic program specialisation.
Higher-Order and Symbolic Computation, 2008

ProB gets Nauty: Effective Symmetry Reduction for B and Z Models.
Proceedings of the Second IEEE/IFIP International Symposium on Theoretical Aspects of Software Engineering, 2008

Declarative programming for verification: lessons and outlook.
Proceedings of the 10th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2008

Fast Offline Partial Evaluation of Large Logic Programs.
Proceedings of the Logic-Based Program Synthesis and Transformation, 2008

The MEB and CEB Static Analysis for CSP Specifications.
Proceedings of the Logic-Based Program Synthesis and Transformation, 2008

Probing the Depths of CSP-M: A New fdr-Compliant Validation Tool.
Proceedings of the Formal Methods and Software Engineering, 2008

Towards Demonstrably Correct Compilation of Java Byte Code.
Proceedings of the Formal Methods for Components and Objects, 7th International Symposium, 2008

The High Road to Formal Validation: .
Proceedings of the Abstract State Machines, B and Z, First International Conference, 2008

2007
Symmetry Reduced Model Checking for B.
Proceedings of the First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, 2007

Automatic Testing from Formal Specifications.
Proceedings of the Tests and Proofs, First International Conference, 2007

Partial Evaluation of Pointcuts.
Proceedings of the Practical Aspects of Declarative Languages, 9th International Symposium, 2007

Seven at one stroke: LTL model checking for High-level Specifications in B, Z, CSP, and more.
Proceedings of the ISoLA 2007, 2007

Validating Z Specifications Using the ProBAnimator and Model Checker.
Proceedings of the Integrated Formal Methods, 6th International Conference, 2007

Animating and Model Checking B Specifications with Higher-Order Recursive Functions.
Proceedings of the Rigorous Methods for Software Construction and Analysis, 07.05., 2007

Symmetry Reduction for B by Permutation Flooding.
Proceedings of the B 2007: Formal Specification and Development in B, 2007

BE4: The B Extensible Eclipse Editing Environment.
Proceedings of the B 2007: Formal Specification and Development in B, 2007

A Generic Flash-Based Animation Engine for ProB.
Proceedings of the B 2007: Formal Specification and Development in B, 2007

Efficient Approximate Verification of Promela Models Via Symmetry Markers.
Proceedings of the Automated Technology for Verification and Analysis, 2007

2006
Rapid Visualization of B Specifications containing Higher-Order Recursive Functions.
Softwaretechnik-Trends, 2006

The Ecce and Logen partial evaluators and their web interfaces.
Proceedings of the 2006 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, 2006

Supervising Offline Partial Evaluation of Logic Programs Using Online Techniques.
Proceedings of the Logic-Based Program Synthesis and Transformation, 2006

2005
Guest Editorial.
Formal Asp. Comput., 2005

ProTest: An Automatic Test Environment for B Specifications.
Electr. Notes Theor. Comput. Sci., 2005

Visualising Larger State Spaces in Pro B.
Proceedings of the ZB 2005: Formal Specification and Development in Z and B, 2005

Self-tuning resource aware specialisation for prolog.
Proceedings of the 7th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2005

Towards Provably Correct Code Generation via Horn Logical Continuation Semantics.
Proceedings of the Practical Aspects of Declarative Languages, 7th International Symposium, 2005

Automatic Refinement Checking for B.
Proceedings of the Formal Methods and Software Engineering, 2005

Combining CSP and B for Specification and Property Verification.
Proceedings of the FM 2005: Formal Methods, 2005

Forward Slicing by Conjunctive Partial Deduction and Argument Filtering.
Proceedings of the Programming Languages and Systems, 2005

Tools for System Validation with B Abstract Machines.
Proceedings of the 12th International Workshop on Abstract State Machines, 2005

2004
Introduction to the Special Issue on Verification and Computational Logic.
TPLP, 2004

Offline specialisation in Prolog using a hand-written compiler generator.
TPLP, 2004

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

Model checking object petri nets in prolog.
Proceedings of the 6th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2004

Efficient and flexible access control via logic program specialisation.
Proceedings of the 2004 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, 2004

Binding-Time Analysis for Mercury.
Proceedings of the Program Development in Computational Logic: A Decade of Research Advances in Logic-Based Program Development, 2004

Specialising Interpreters Using Offline Partial Deduction.
Proceedings of the Program Development in Computational Logic: A Decade of Research Advances in Logic-Based Program Development, 2004

Fully Automatic Binding-Time Analysis for Prolog.
Proceedings of the Logic Based Program Synthesis and Transformation, 2004

PROB: un outil de modélisation formelle.
Proceedings of the Programmation en logique avec contraintes, 2004

The Use of Formal Methods in the Analysis of Trust (Position Paper).
Proceedings of the Trust Management, Second International Conference, 2004

LIX: an Effective Self-applicable Partial Evaluator for Prolog.
Proceedings of the Functional and Logic Programming, 7th International Symposium, 2004

A Trust Analysis Methodology for Pervasive Computing Systems.
Proceedings of the Trusting Agents for Trusting Electronic Societies, 2004

2003
Model-Based Approaches for Validating Business Critical Systems.
Proceedings of the 11th International Workshop on Software Technology and Engineering Practice (STEP 2003), 2003

Inductive Theorem Proving by Program Specialisation: Generating Proofs for Isabelle Using Ecce.
Proceedings of the Logic Based Program Synthesis and Transformation, 2003

Partial Evaluation of MATLAB.
Proceedings of the Generative Programming and Component Engineering, 2003

ProB: A Model Checker for B.
Proceedings of the FME 2003: Formal Methods, 2003

A Compiler Generator for Constraint Logic Programs.
Proceedings of the Perspectives of Systems Informatics, 2003

The Benefits of Rapid Modelling for E-business System Development.
Proceedings of the Conceptual Modeling for Novel Application Domains, 2003

2002
Logic program specialisation through partial deduction: Control issues.
TPLP, 2002

Book Reviews.
Softw. Test., Verif. Reliab., 2002

Homeomorphic Embedding for Online Termination of Symbolic Methods.
Proceedings of the Essence of Computation, Complexity, Analysis, 2002

2001
Design and Implementation of the High-Level Specification Language CSP(LP) in Prolog.
Proceedings of the Practical Aspects of Declarative Languages, 2001

Abstract Conjunctive Partial Deduction Using Regular Types and Its Application to Model Checking.
Proceedings of the Logic Based Program Synthesis and Transformation, 2001

How to Make FDR Spin LTL Model Checking of CSP by Refinement.
Proceedings of the FME 2001: Formal Methods for Increasing Software Productivity, 2001

2000
Erratum to: "Conjunctive Partial Deduction: Foundations, Control, Algorithms and Experiments".
J. Log. Program., 2000

Solving coverability problems of petri nets by partial deduction.
Proceedings of the 2nd international ACM SIGPLAN conference on on Principles and practice of declarative programming, 2000

Solving Planning Problems by Partial Deduction.
Proceedings of the Logic for Programming and Automated Reasoning, 2000

Coverability of Reset Petri Nets and Other Well-Structured Transition Systems by Partial Deduction.
Proceedings of the Computational Logic, 2000

Decidability Results for the Propositional Fluent Calculus.
Proceedings of the Computational Logic, 2000

1999
Efficient Specialisation in Prolog Using the Hand-Written Compiler Generator LOGEN.
Electr. Notes Theor. Comput. Sci., 1999

Preface - Workshop on Optimization and Implementation of Declarative Programs.
Electr. Notes Theor. Comput. Sci., 1999

Conjunctive Partial Deduction: Foundations, Control, Algorithms, and Experiments.
J. Log. Program., 1999

Infinite State Model Checking by Abstract Interpretation and Program Specialisation.
Proceedings of the Logic Programming Synthesis and Transformation, 1999

Sonic Partial Deduction.
Proceedings of the Perspectives of System Informatics, 1999

Abstraction-Based Partial Deduction for Solving Inverse Problems - A Transformational Approach to Software Verification.
Proceedings of the Perspectives of System Informatics, 1999

1998
Controlling Generalization amd Polyvariance in Partial Deduction of Normal Logic Programs.
ACM Trans. Program. Lang. Syst., 1998

Constrained Partial Deduction and the Preservation of Characteristic Trees.
New Generation Comput., 1998

Creating Specialised Integrity Checks Through Partial Evaluation of Meta-Interpreters.
J. Log. Program., 1998

Extending Partial Deduction to Tabled Execution: Some Results and Open Issues.
ACM Comput. Surv., 1998

Some Achievements and Prospects in Partial Deduction.
ACM Comput. Surv., 1998

On the Power of Homeomorphic Embedding for Online Termination.
Proceedings of the Static Analysis, 5th International Symposium, 1998

Advanced Logic Program Specialisation.
Proceedings of the Partial Evaluation - Practice and Theory, DIKU 1998 International Summer School, Copenhagen, Denmark, June 29, 1998

Logic Program Specialisation.
Proceedings of the Partial Evaluation - Practice and Theory, DIKU 1998 International Summer School, Copenhagen, Denmark, June 29, 1998

Improving Homeomorphic Embedding for Online Termination.
Proceedings of the Logic Programming Synthesis and Transformation, 1998

Program Specialisation and Abstract Interpretation Reconciled.
Proceedings of the 1998 Joint International Conference and Symposium on Logic Programming, 1998

A Polyvariant Binding-Time Analysis for Off-line Partial Deduction.
Proceedings of the Programming Languages and Systems - ESOP'98, 7th European Symposium on Programming, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'98, Lisbon, Portugal, March 28, 1998

1997
Advanced Techniques for Logic Program Specialisation.
AI Commun., 1997

Constrained Partial Deduction.
Proceedings of the Twelfth Workshop Logic Programming, 1997

Extending Homeomorphic Embedding in the Context of Logic Programming.
Proceedings of the Twelfth Workshop Logic Programming, 1997

Specialization of Declarative Programs and Its Applications (Workshop Overview).
Proceedings of the Logic Programming, 1997

Preserving Termination of Tabled Logic Programs While Unfolding.
Proceedings of the Logic Programming Synthesis and Transformation, 1997

Termination Analysis for Tabled Logic Programming.
Proceedings of the Logic Programming Synthesis and Transformation, 1997

1996
Logic Program Specialisation: How To Be More Specific.
Proceedings of the Programming Languages: Implementations, 1996

Redundant Argument Filtering of Logic Programs.
Proceedings of the Logic Programming Synthesis and Transformation, 1996

Logic Program Specialisation: How to Be More Specific (Abstract).
Proceedings of the Logic Programming Synthesis and Transformation, 1996

Conjunctive Partial Deduction in Practice.
Proceedings of the Logic Programming Synthesis and Transformation, 1996

A Conceptual Embedding of Folding into Partial Deduction: Towards a Maximal Integration.
Proceedings of the Logic Programming, 1996

Global Control for Partial Deduction through Characteristic Atoms and Global Trees.
Proceedings of the Partial Evaluation, International Seminar, 1996

Efficiently Generating Efficient Generating Extensions in Prolog.
Proceedings of the Partial Evaluation, International Seminar, 1996

1995
Tutorial on Program Specialisation (Abstract).
Proceedings of the Logic Programming, 1995

Partial Deduction of the Ground Representation and its Application to Integrity Checking.
Proceedings of the Logic Programming, 1995

Towards Creating Specialised Integrity Checks through Partial Evaluation of Meta-Interpreters.
Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, 1995

Ecological Partial Deduction: Preserving Characteristic Trees Without Constraints.
Proceedings of the Logic Programming Synthesis and Transformation, 1995

Generating Specialised Update Procedures Through Partial Deduction of the Ground Representation.
Proceedings of the Deductive Databases and Logic Programming, 1995

1994
Partial Evaluation of the "Real Thing".
Proceedings of the Logic Programming Synthesis and Transformation, 1994


  Loading...