![](https://dblp.uni-trier.de/img/logo.ua.320x120.png)
![](https://dblp.uni-trier.de/img/dropdown.dark.16x16.png)
![](https://dblp.uni-trier.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
![search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
default search action
Michael Leuschel
Person information
- affiliation: University of Düsseldorf, Germany
Refine list
![note](https://dblp.uni-trier.de/img/note-mark.dark.12x12.png)
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
Journal Articles
- 2024
- [j48]Sebastian Stock
, Atif Mashkoor
, Michael Leuschel
, Alexander Egyed
:
Trace preservation in B and Event-B refinements. J. Log. Algebraic Methods Program. 137: 100943 (2024) - [j47]Fabian Vu
, Christopher Happe, Michael Leuschel
:
Generating interactive documents for domain-specific validation of formal models. Int. J. Softw. Tools Technol. Transf. 26(2): 147-168 (2024) - 2022
- [j46]Joshua Schmidt
, Michael Leuschel
:
SMT solving for the validation of B and Event-B models. Int. J. Softw. Tools Technol. Transf. 24(6): 1043-1077 (2022) - [j45]David Geleßus
, Michael Leuschel:
Making ProB Compatible with SWI-Prolog. Theory Pract. Log. Program. 22(5): 755-769 (2022) - [j44]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
:
Fifty Years of Prolog and Beyond. Theory Pract. Log. Program. 22(6): 776-858 (2022) - 2021
- [j43]Philipp Körner
, Jens Bendisposto
, Jannik Dunkelau
, Sebastian Krings
, Michael Leuschel
:
Integrating formal specifications into applications: the ProB Java API. Formal Methods Syst. Des. 58(1-2): 160-187 (2021) - 2020
- [j42]Sebastian Krings
, Michael Leuschel, Joshua Schmidt
, David Schneider, Marc Frappier:
Translating Alloy and extensions to classical B. Sci. Comput. Program. 188: 102378 (2020) - [j41]Dominik Hansen, Michael Leuschel, Philipp Körner
, Sebastian Krings, Thomas Naulin, Nader Nayeri, David Schneider, Frank Skowron:
Validation and real-life demonstration of ETCS hybrid level 3 principles using a formal B model. Int. J. Softw. Tools Technol. Transf. 22(3): 315-332 (2020) - 2018
- [j40]David Schneider, Michael Leuschel
, Tobias Witt:
Model-based problem solving for university timetable validation and improvement. Formal Aspects Comput. 30(5): 545-569 (2018) - [j39]Sebastian Krings
, Michael Leuschel:
Proof assisted bounded and unbounded symbolic model checking of software and system models. Sci. Comput. Program. 158: 41-63 (2018) - [j38]Ivaylo Dobrikov
, Michael Leuschel:
Enabling analysis for Event-B. Sci. Comput. Program. 158: 81-99 (2018) - 2017
- [j37]Sebastian Krings
, Michael Leuschel:
Inferring physical units in formal models. Softw. Syst. Model. 16(1): 25-47 (2017) - [j36]Lukas Ladenberger, Dominik Hansen, Harald Wiegard, Jens Bendisposto, Michael Leuschel:
Validation of the ABZ landing gear system using ProB. Int. J. Softw. Tools Technol. Transf. 19(2): 187-203 (2017) - 2016
- [j35]Ivaylo Dobrikov, Michael Leuschel:
Optimising the ProB model checker for B using partial order reduction. Formal Aspects Comput. 28(2): 295-323 (2016) - [j34]Dominik Hansen, Michael Leuschel:
Translating B to TLA+ for validation with TLC. Sci. Comput. Program. 131: 109-125 (2016) - 2014
- [j33]Michael Leuschel, Germán Vidal
:
Fast offline partial evaluation of logic programs. Inf. Comput. 235: 70-97 (2014) - [j32]Jens Bendisposto, Michael Leuschel, Markus Roggenbach
:
Preface of Automated Verification of Critical Systems 2010 (AVoCS 2010). Sci. Comput. Program. 81: 1-2 (2014) - [j31]Michael Leuschel, Tom Schrijvers
:
Introduction to the 30th International Conference on Logic Programming Special Issue. Theory Pract. Log. Program. 14(4-5): 401-414 (2014) - 2013
- [j30]Stefan Hallerstede, Michael Leuschel, Daniel Plagge:
Validation of formal models by refinement animation. Sci. Comput. Program. 78(3): 272-292 (2013) - 2012
- [j29]Stefan Hallerstede, Michael Leuschel:
Experiments in program verification using Event-B. Formal Aspects Comput. 24(1): 97-125 (2012) - [j28]Michael Leuschel, Marisa Llorens
, Javier Oliver
, Josep Silva
, Salvador Tamarit
:
Static slicing of explicitly synchronized languages. Inf. Comput. 214: 10-46 (2012) - 2011
- [j27]Alexander B. Romanovsky
, Cliff B. Jones, Jens Bendisposto, Michael Leuschel:
Preface. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 46 (2011) - [j26]Michael Leuschel, Jérôme Falampin, Fabian Fritz, Daniel Plagge:
Automated property verification for large scale B models with ProB. Formal Aspects Comput. 23(6): 683-709 (2011) - [j25]Michael Leuschel, Heike Wehrheim:
Selected papers on Integrated Formal Methods (iFM09). Sci. Comput. Program. 76(10): 835-836 (2011) - [j24]Jens Bendisposto, Fabian Fritz, Michael Jastram, Michael Leuschel, Ingo Weigelt:
Developing Camille, a text editor for Rodin. Softw. Pract. Exp. 41(2): 189-198 (2011) - [j23]Stefan Hallerstede, Michael Leuschel:
Constraint-based deadlock checking of high-level specifications. Theory Pract. Log. Program. 11(4-5): 767-782 (2011) - 2010
- [j22]Michael Leuschel, Thierry Massart:
Efficient approximate verification of B and Z models via symmetry markers. Ann. Math. Artif. Intell. 59(1): 81-106 (2010) - [j21]Jens Bendisposto, Michael Leuschel, Markus Roggenbach:
Avocs2010 Preface. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 35 (2010) - [j20]Daniel Plagge, Michael Leuschel:
Seven at one stroke: LTL model checking for high-level specifications in B, Z, CSP, and more. Int. J. Softw. Tools Technol. Transf. 12(1): 9-21 (2010) - 2008
- [j19]Julia Lawall, Michael Leuschel, Peter Sestoft:
Editorial. High. Order Symb. Comput. 21(1-2): 1-3 (2008) - [j18]Steve Barker, Michael Leuschel, Mauricio Varea:
Efficient and flexible access control via Jones-optimal logic program specialisation. High. Order Symb. Comput. 21(1-2): 5-35 (2008) - [j17]Michael Leuschel, Michael J. Butler
:
ProB: an automated analysis toolset for the B method. Int. J. Softw. Tools Technol. Transf. 10(2): 185-203 (2008) - [j16]Jens Bendisposto, Michael Leuschel, O. Ligot, Mireille Samia:
La validation de modèles Event-B avec le plug-in ProB pour RODIN. Tech. Sci. Informatiques 27(8): 1065-1084 (2008) - 2006
- [j15]Jens Bendisposto, Michael Leuschel:
Rapid Visualization of B Specifications containing Higher-Order Recursive Functions. Softwaretechnik-Trends 26(2) (2006) - 2005
- [j14]Michael Leuschel:
Guest Editorial. Formal Aspects Comput. 17(2): 91-92 (2005) - 2004
- [j13]Michael Leuschel:
A framework for the integration of partial evaluation and abstract interpretation of logic programs. ACM Trans. Program. Lang. Syst. 26(3): 413-463 (2004) - [j12]Michael Leuschel, Jesper Jørgensen, Wim Vanhoof
, Maurice Bruynooghe:
Offline specialisation in Prolog using a hand-written compiler generator. Theory Pract. Log. Program. 4(1-2): 139-191 (2004) - [j11]Michael Leuschel, Andreas Podelski, C. R. Ramakrishnan, Ulrich Ultes-Nitsche
:
Introduction to the Special Issue on Verification and Computational Logic. Theory Pract. Log. Program. 4(5-6): 543-544 (2004) - 2002
- [j10]Michael Leuschel:
Book Reviews. Softw. Test. Verification Reliab. 12(3): 187-188 (2002) - [j9]Michael Leuschel, Maurice Bruynooghe:
Logic program specialisation through partial deduction: Control issues. Theory Pract. Log. Program. 2(4-5): 461-515 (2002) - 2000
- [j8]Danny De Schreye
, Robert Glück, Jesper Jørgensen, Michael Leuschel, Bern Martens, Morten Heine Sørensen:
Erratum to: "Conjunctive Partial Deduction: Foundations, Control, Algorithms and Experiments". J. Log. Program. 43(3): 265 (2000) - 1999
- [j7]Danny De Schreye
, Robert Glück
, Jesper Jørgensen, Michael Leuschel, Bern Martens, Morten Heine Sørensen:
Conjunctive Partial Deduction: Foundations, Control, Algorithms, and Experiments. J. Log. Program. 41(2-3): 231-277 (1999) - 1998
- [j6]Michael Leuschel, Bern Martens, Danny De Schreye
:
Some Achievements and Prospects in Partial Deduction. ACM Comput. Surv. 30(3es): 4 (1998) - [j5]Konstantinos Sagonas
, Michael Leuschel:
Extending Partial Deduction to Tabled Execution: Some Results and Open Issues. ACM Comput. Surv. 30(3es): 16 (1998) - [j4]Michael Leuschel, Danny De Schreye
:
Creating Specialised Integrity Checks Through Partial Evaluation of Meta-Interpreters. J. Log. Program. 36(2): 149-193 (1998) - [j3]Michael Leuschel, Danny De Schreye
:
Constrained Partial Deduction and the Preservation of Characteristic Trees. New Gener. Comput. 16(3): 283-342 (1998) - [j2]Michael Leuschel, Bern Martens, Danny De Schreye
:
Controlling Generalization amd Polyvariance in Partial Deduction of Normal Logic Programs. ACM Trans. Program. Lang. Syst. 20(1): 208-258 (1998) - 1997
- [j1]Michael Leuschel:
Advanced Techniques for Logic Program Specialisation. AI Commun. 10(2): 127-128 (1997)
Conference and Workshop Papers
- 2024
- [c165]Fabian Vu
, Jannik Dunkelau
, Michael Leuschel
:
Validation of Reinforcement Learning Agents and Safety Shields with ProB. NFM 2024: 279-297 - 2023
- [c164]Jannik Dunkelau
, Michael Leuschel
:
Performance Fuzzing with Reinforcement-Learning and Well-Defined Constraints for the B Method. iFM 2023: 237-256 - [c163]Jan Gruteser, David Geleßus
, Michael Leuschel
, Jan Roßbach, Fabian Vu
:
A Formal Model of Train Control with AI-Based Obstacle Detection. RSSRail 2023: 128-145 - [c162]Michael Leuschel
, Nader Nayeri:
Modelling, Visualisation and Proof of an ETCS Level 3 Moving Block System. RSSRail 2023: 193-210 - [c161]Fabian Vu
, Michael Leuschel
:
Validation of Formal Models by Interactive Simulation. ABZ 2023: 59-69 - [c160]Sebastian Stock
, Fabian Vu
, David Geleßus
, Michael Leuschel
, Atif Mashkoor
, Alexander Egyed
:
Validation by Abstraction and Refinement. ABZ 2023: 160-178 - [c159]David Geleßus
, Sebastian Stock
, Fabian Vu
, Michael Leuschel
, Atif Mashkoor
:
Modeling and Analysis of a Safety-Critical Interactive System Through Validation Obligations. ABZ 2023: 284-302 - [c158]Amel Mammar
, Michael Leuschel
:
Modeling and Verifying an Arrival Manager Using Event-B. ABZ 2023: 321-339 - [c157]Jan Roßbach, Michael Leuschel:
Certified Control for Train Sign Classification. FMAS@iFM 2023: 69-76 - 2022
- [c156]Fabian Vu
, Christopher Happe, Michael Leuschel
:
Generating Domain-Specific Interactive Validation Documents. FMICS 2022: 32-49 - [c155]Sebastian Stock
, Atif Mashkoor
, Michael Leuschel
, Alexander Egyed
:
Trace Refinement in B and Event-B. ICFEM 2022: 316-333 - [c154]Fabian Vu
, Dominik Brandt, Michael Leuschel
:
Model Checking B Models via High-Level Code Generation. ICFEM 2022: 334-351 - [c153]Michael Leuschel
:
Operation Caching and State Compression for Model Checking of High-Level Models - How to Have Your Cake and Eat It. IFM 2022: 129-145 - [c152]Philipp Körner
, Michael Leuschel
:
Towards Practical Partial Order Reduction for High-Level Formalisms. VSTTE 2022: 72-91 - 2021
- [c151]Fabian Vu
, Michael Leuschel
, Atif Mashkoor
:
Validation of Formal Models by Timed Probabilistic Simulation. ABZ 2021: 81-96 - [c150]Michael Leuschel
:
Spot the Difference: A Detailed Comparison Between B and Event-B. Logic, Computation and Rigorous Methods 2021: 147-172 - [c149]Joshua Schmidt
, Michael Leuschel
:
Improving SMT Solver Integrations for the Validation of B and Event-B Models. FMICS 2021: 107-125 - [c148]Jens Bendisposto
, David Geleßus, Yumiko Jansing, Michael Leuschel
, Antonia Pütz, Fabian Vu
, Michelle Werth:
ProB2-UI: A Java-Based User Interface for ProB. FMICS 2021: 193-201 - [c147]Atif Mashkoor, Michael Leuschel, Alexander Egyed:
Validation Obligations: A Novel Approach to Check Compliance between Requirements and their Formal Specification. ICSE (NIER) 2021: 1-5 - 2020
- [c146]Jannik Dunkelau
, Joshua Schmidt
, Michael Leuschel
:
Analysing ProB's Constraint Solving Backends - What Do They Know? Do They Know Things? Let's Find Out! ABZ 2020: 107-123 - [c145]David Geleßus, Michael Leuschel
:
ProB and Jupyter for Logic, Set Theory, Theoretical Computer Science and Formal Methods. ABZ 2020: 248-254 - [c144]Michelle Werth, Michael Leuschel:
VisB: A Lightweight Tool to Visualize Formal Models with SVG Graphics. ABZ 2020: 260-265 - [c143]Philipp Körner
, Michael Leuschel
, Jannik Dunkelau
:
Towards a Shared Specification Repository. ABZ 2020: 266-271 - [c142]Michael Leuschel, Mareike Mutz, Michelle Werth:
Modelling and Validating an Automotive System in Classical B and Event-B. ABZ 2020: 335-350 - [c141]Michael J. Butler
, Philipp Körner
, Sebastian Krings
, Thierry Lecomte
, Michael Leuschel
, Luis-Fernando Mejia, Laurent Voisin
:
The First Twenty-Five Years of Industrial Use of the B-Method. FMICS 2020: 189-209 - [c140]Michael Leuschel
:
Fast and Effective Well-Definedness Checking. IFM 2020: 63-81 - [c139]Philipp Körner
, David Schneider, Michael Leuschel
:
On the Performance of Bytecode Interpreters in Prolog. WFLP 2020: 41-56 - [c138]Michael Leuschel:
Prolog for Verification, Analysis and Transformation Tools. VPT/HCVS@ETAPS 2020: 80-94 - 2019
- [c137]Philipp Körner
, Jens Bendisposto
, Jannik Dunkelau
, Sebastian Krings
, Michael Leuschel
:
Embedding High-Level Formal Specifications into Applications. FM 2019: 519-535 - [c136]Sebastian Krings
, Michael Leuschel
:
Embedding SMT-LIB into B for Interactive Proof and Constraint Solving. IFM 2019: 265-283 - [c135]Fabian Vu
, Dominik Hansen, Philipp Körner
, Michael Leuschel
:
A Multi-target Code Generator for High-Level B. IFM 2019: 456-473 - [c134]Mathieu Comptier, Michael Leuschel, Luis-Fernando Mejia, Julien Molinero Perez, Mareike Mutz:
Property-Based Modelling and Validation of a CBTC Zone Controller in Event-B. RSSRail 2019: 202-212 - [c133]Akram Idani, Germán Vega, Michael Leuschel:
Applying Formal Reasoning to Model Transformation: The Meeduse solution. TTC@STAF 2019: 33-44 - 2018
- [c132]Sebastian Krings
, Joshua Schmidt, Carola Brings, Marc Frappier, Michael Leuschel:
A Translation from Alloy to B. ABZ 2018: 71-86 - [c131]Dominik Hansen, Michael Leuschel, David Schneider, Sebastian Krings
, Philipp Körner
, Thomas Naulin, Nader Nayeri, Frank Skowron:
Using a Formal B Model at Runtime in a Demonstration of the ETCS Hybrid Level 3 Concept with Real Trains. ABZ 2018: 292-306 - [c130]Lionel N. Tidjon
, Marc Frappier, Michael Leuschel, Amel Mammar:
Extended Algebraic State-Transition Diagrams. ICECCS 2018: 146-155 - [c129]Philipp Körner
, Michael Leuschel, Jeroen Meijer:
State-of-the-Art Model Checking for B and Event-B Using ProB and LTSmin. IFM 2018: 275-295 - [c128]Joshua Schmidt, Sebastian Krings
, Michael Leuschel:
Repair and Generation of Formal Models Using Synthesis. IFM 2018: 346-366 - [c127]Steve Jeffrey Tueno Fotso, Marc Frappier, Régine Laleau, Amel Mammar, Michael Leuschel:
Formalisation of SysML/KAOS Goal Assignments with B System Component Decompositions. IFM 2018: 377-397 - [c126]Sebastian Krings
, Michael Leuschel
, Philipp Körner
, Stefan Hallerstede
, Miran Hasanagic
:
Three Is a Crowd: SAT, SMT and CLP on a Chessboard. PADL 2018: 63-79 - [c125]Stefan Hallerstede, Miran Hasanagic, Sebastian Krings
, Peter Gorm Larsen
, Michael Leuschel:
From Software Specifications to Constraint Programming. SEFM 2018: 21-36 - [c124]Michael Leuschel:
Solving Set Constraints in B and Event-B: Foundations and Applications (invited talk). SETS@ABZ 2018: 1 - 2017
- [c123]Sebastian Krings
, Michael Leuschel:
Constraint Logic Programming over Infinite Domains with an Application to Proof. WLP / WFLP 2017: 73-87 - 2016
- [c122]Ivaylo Dobrikov, Michael Leuschel:
Enabling Analysis for Event-B. ABZ 2016: 102-118 - [c121]Michael Leuschel, Egon Börger:
A Compact Encoding of Sequential ASMs in Event-B. ABZ 2016: 119-134 - [c120]Sebastian Krings
, Michael Leuschel:
Proof Assisted Symbolic Model Checking for B and Event-B. ABZ 2016: 135-150 - [c119]Dominik Hansen, David Schneider, Michael Leuschel:
Using B and ProB for Data Validation Projects. ABZ 2016: 167-182 - [c118]Joy Clark, Jens Bendisposto, Stefan Hallerstede, Dominik Hansen, Michael Leuschel:
Generating Event-B Specifications from Algorithm Descriptions. ABZ 2016: 183-197 - [c117]Joshua Schmidt, Sebastian Krings
, Michael Leuschel:
Interactive Model Repair by Synthesis. ABZ 2016: 303-307 - [c116]Jens Bendisposto, Philipp Körner
, Michael Leuschel, Jeroen Meijer, Jaco van de Pol, Helen Treharne
, Jorden Whitefield
:
Symbolic Reachability Analysis of B Through ProB and LTSmin. IFM 2016: 275-291 - [c115]Sebastian Krings
, Michael Leuschel:
SMT Solvers for Validation of B and Event-B Models. IFM 2016: 361-375 - [c114]Michael Leuschel:
Formal Model-Based Constraint Solving and Document Generation. SBMF 2016: 3-20 - [c113]Ivaylo Dobrikov, Michael Leuschel, Daniel Plagge:
LTL Model Checking under Fairness in ProB. SEFM 2016: 204-211 - [c112]Lukas Ladenberger, Michael Leuschel:
BMotionWeb: A Tool for Rapid Creation of Formal Prototypes. SEFM 2016: 403-417 - 2015
- [c111]David Schneider, Michael Leuschel, Tobias Witt:
Model-Based Problem Solving for University Timetable Validation and Improvement. FM 2015: 487-495 - [c110]Lukas Ladenberger, Michael Leuschel:
Mastering the Visualization of Larger State Spaces with Projection Diagrams. ICFEM 2015: 153-169 - [c109]Aymerick Savary, Marc Frappier, Michael Leuschel, Jean-Louis Lanet:
Model-Based Robustness Testing in Event-B Using Mutation. SEFM 2015: 132-147 - [c108]Sebastian Krings
, Jens Bendisposto, Michael Leuschel:
From Failure to Proof: The ProB Disprover for B and Event-B. SEFM 2015: 199-214 - 2014
- [c107]Dominik Hansen, Michael Leuschel:
Translating B to TLA + for Validation with TLC. ABZ 2014: 40-55 - [c106]Dominik Hansen, Lukas Ladenberger, Harald Wiegard, Jens Bendisposto, Michael Leuschel:
Validation of the ABZ Landing Gear System Using ProB. ABZ (Case Study) 2014: 66-79 - [c105]Michael Leuschel, David Schneider:
Towards B as a High-Level Constraint Modelling Language - Solving the Jobs Puzzle Challenge. ABZ 2014: 101-116 - [c104]Michael Leuschel:
Towards Constraint-Solving over Higher-Order Unbounded Datatypes using Formal Methods Tools. VPT@CAV 2014: 1 - [c103]Lukas Ladenberger, Ivaylo Dobrikov, Michael Leuschel:
An Approach for Creating Domain Specific Visualisations of CSP Models. SEFM Workshops 2014: 20-35 - [c102]Ivaylo Dobrikov, Michael Leuschel:
Optimising the ProB Model Checker for B Using Partial Order Reduction. SEFM 2014: 220-234 - [c101]Jens Bendisposto, Sebastian Krings
, Michael Leuschel:
Who watches the watchers: Validating the ProB Validation Tool. F-IDE 2014: 16-29 - [c100]John Witulski, Michael Leuschel:
Checking Computations of Formal Method Tools - A Secondary Toolchain for ProB. F-IDE 2014: 93-105 - 2013
- [c99]Sebastian Krings
, Michael Leuschel:
Inferring Physical Units in B Models. SEFM 2013: 137-151 - 2012
- [c98]Daniel Plagge, Michael Leuschel:
Validating B, Z and TLA + Using ProB and Kodkod. FM 2012: 372-386 - [c97]Dominik Hansen, Michael Leuschel:
Translating TLA + to B for Validation with ProB. IFM 2012: 24-38 - 2011
- [c96]Carl Friedrich Bolz, Antonio Cuni, Maciej Fijalkowski, Michael Leuschel, Samuele Pedroni, Armin Rigo:
Runtime feedback in a meta-tracing JIT for efficient dynamic languages. ICOOOLPS@ECOOP 2011: 9:1-9:8 - [c95]Jens Bendisposto, Michael Leuschel:
Automatic Flow Analysis for Event-B. FASE 2011: 50-64 - [c94]Rainer Gmehlich, Katrin Grau, Stefan Hallerstede, Michael Leuschel, Felix Lösch, Daniel Plagge:
On Fitting a Formal Method into Practice. ICFEM 2011: 195-210 - [c93]Carl Friedrich Bolz
, Antonio Cuni, Maciej Fijalkowski, Michael Leuschel, Samuele Pedroni, Armin Rigo:
Allocation removal by partial evaluation in a tracing JIT. PEPM 2011: 43-52 - 2010
- [c92]Edd Turner, Michael J. Butler
, Michael Leuschel:
A Refinement-Based Correctness Proof of Symmetry Reduced Model Checking. ASM 2010: 231-244 - [c91]Stefan Hallerstede, Michael Leuschel, Daniel Plagge:
Refinement-Animation for Event-B - Towards a Method of Validation. ASM 2010: 287-301 - [c90]Carl Friedrich Bolz
, Michael Leuschel, David Schneider:
Towards a jitting VM for prolog execution. PPDP 2010: 99-108 - [c89]Michael Leuschel, Jens Bendisposto:
Directed Model Checking for B: An Evaluation and New Techniques. SBMF 2010: 1-16 - [c88]Michael Jastram, Stefan Hallerstede, Michael Leuschel, Aryldo G. Russo:
An Approach of Requirements Tracing in Formal Refinement. VSTTE 2010: 97-111 - 2009
- [c87]Michael Leuschel, Dominique Cansell, Michael J. Butler
:
Validating and Animating Higher-Order Recursive Functions in B. Rigorous Methods for Software Construction and Analysis 2009: 78-92 - [c86]Michael Leuschel, Jérôme Falampin, Fabian Fritz, Daniel Plagge:
Automated Property Verification for Large Scale B Models. FM 2009: 708-723 - [c85]Lukas Ladenberger, Jens Bendisposto, Michael Leuschel:
Visualising Event-B Models with B-Motion Studio. FMICS 2009: 202-204 - [c84]Jens Bendisposto, Michael Leuschel:
Proof Assisted Model Checking for B. ICFEM 2009: 504-520 - [c83]Mireille Samia, Michael Leuschel:
Towards pie tree visualization of graphs and large software architectures. ICPC 2009: 301-302 - [c82]Carl Friedrich Bolz
, Michael Leuschel, Armin Rigo:
Towards Just-In-Time Partial Evaluation of Prolog. LOPSTR 2009: 158-172 - [c81]Michael Leuschel, Marisa Llorens
, Javier Oliver
, Josep Silva
, Salvador Tamarit
:
SOC: a slicer for CSP specifications. PEPM 2009: 165-168 - [c80]Sebastian Wieczorek, Vitaly Kozyura, Andreas Roth, Michael Leuschel, Jens Bendisposto, Daniel Plagge, Ina Schieferdecker
:
Applying Model Checking to Generate Model-Based Integration Tests from Choreography Models. TestCom/FATES 2009: 179-194 - [c79]Mireille Samia, Michael Leuschel:
Pie Tree Visualization. SEKE 2009: 400-405 - [c78]Stefan Hallerstede, Michael Leuschel:
How to Explain Mistakes. TFM 2009: 105-124 - [c77]Michael Leuschel, Salvador Tamarit
, Germán Vidal
:
Fast and Accurate Strong Termination Analysis with an Application to Partial Evaluation. WFLP 2009: 111-127 - 2008
- [c76]Michael Leuschel:
The High Road to Formal Validation: . ABZ 2008: 4-23 - [c75]Michael Leuschel:
Towards Demonstrably Correct Compilation of Java Byte Code. FMCO 2008: 119-138 - [c74]Michael Leuschel, Marc Fontaine:
Probing the Depths of CSP-M: A New fdr-Compliant Validation Tool. ICFEM 2008: 278-297 - [c73]Michael Leuschel, Marisa Llorens
, Javier Oliver
, Josep Silva
, Salvador Tamarit
:
The MEB and CEB Static Analysis for CSP Specifications. LOPSTR 2008: 103-118 - [c72]Michael Leuschel, Germán Vidal
:
Fast Offline Partial Evaluation of Large Logic Programs. LOPSTR 2008: 119-134 - [c71]Michael Leuschel:
Declarative programming for verification: lessons and outlook. PPDP 2008: 1-7 - [c70]Corinna Spermann, Michael Leuschel:
ProB gets Nauty: Effective Symmetry Reduction for B and Z Models. TASE 2008: 15-22 - 2007
- [c69]Dragan Bosnacki, Alastair F. Donaldson, Michael Leuschel, Thierry Massart:
Efficient Approximate Verification of Promela Models Via Symmetry Markers. ATVA 2007: 300-315 - [c68]Michael Leuschel, Michael J. Butler, Corinna Spermann, Edd Turner:
Symmetry Reduction for B by Permutation Flooding. B 2007: 79-93 - [c67]Jens Bendisposto, Michael Leuschel:
A Generic Flash-Based Animation Engine for ProB. B 2007: 266-269 - [c66]Jens Bendisposto, Michael Leuschel:
BE4: The B Extensible Eclipse Editing Environment. B 2007: 270-273 - [c65]Daniel Plagge, Michael Leuschel:
Validating Z Specifications Using the ProBAnimator and Model Checker. IFM 2007: 480-500 - [c64]Michael Leuschel, Daniel Plagge:
Seven at one stroke: LTL model checking for High-level Specifications in B, Z, CSP, and more. ISoLA 2007: 73-84 - [c63]Karl Klose, Klaus Ostermann, Michael Leuschel:
Partial Evaluation of Pointcuts. PADL 2007: 320-334 - [c62]Manoranjan Satpathy, Michael J. Butler, Michael Leuschel, S. Ramesh:
Automatic Testing from Formal Specifications. TAP 2007: 95-113 - [c61]Edd Turner, Michael Leuschel, Corinna Spermann, Michael J. Butler
:
Symmetry Reduced Model Checking for B. TASE 2007: 25-34 - 2006
- [c60]Michael Leuschel, Stephen-John Craig, Daniel Elphick:
Supervising Offline Partial Evaluation of Logic Programs Using Online Techniques. LOPSTR 2006: 43-59 - [c59]Michael Leuschel, Daniel Elphick, Mauricio Varea, Stephen-John Craig, Marc Fontaine:
The Ecce and Logen partial evaluators and their web interfaces. PEPM 2006: 88-94 - 2005
- [c58]Michael J. Butler, Michael Leuschel, Colin F. Snook:
Tools for System Validation with B Abstract Machines. Abstract State Machines 2005: 57-69 - [c57]Michael Leuschel, Germán Vidal:
Forward Slicing by Conjunctive Partial Deduction and Argument Filtering. ESOP 2005: 61-76 - [c56]Michael J. Butler, Michael Leuschel:
Combining CSP and B for Specification and Property Verification. FM 2005: 221-236 - [c55]Michael Leuschel, Michael J. Butler
:
Automatic Refinement Checking for B. ICFEM 2005: 345-359 - [c54]Qian Wang, Gopal Gupta, Michael Leuschel:
Towards Provably Correct Code Generation via Horn Logical Continuation Semantics. PADL 2005: 98-112 - [c53]Stephen-John Craig, Michael Leuschel:
Self-tuning resource aware specialisation for prolog. PPDP 2005: 23-34 - [c52]Michael Leuschel, Edd Turner:
Visualising Larger State Spaces in Pro B. ZB 2005: 6-23 - 2004
- [c51]Stéphane Lo Presti, Michael J. Butler
, Michael Leuschel, Chris Booth:
A Trust Analysis Methodology for Pervasive Computing Systems. Trusting Agents for Trusting Electronic Societies 2004: 129-143 - [c50]Stephen-John Craig, Michael Leuschel:
LIX: an Effective Self-applicable Partial Evaluator for Prolog. FLOPS 2004: 85-99 - [c49]Michael J. Butler, Michael Leuschel, Stéphane Lo Presti, Phillip Turner:
The Use of Formal Methods in the Analysis of Trust (Position Paper). iTrust 2004: 333-339 - [c48]Michael Leuschel:
PROB: un outil de modélisation formelle. JFPLC 2004 - [c47]Stephen-John Craig, John P. Gallagher, Michael Leuschel, Kim S. Henriksen:
Fully Automatic Binding-Time Analysis for Prolog. LOPSTR 2004: 53-68 - [c46]Steve Barker, Michael Leuschel, Mauricio Varea:
Efficient and flexible access control via logic program specialisation. PEPM 2004: 190-199 - [c45]Berndt Farwer, Michael Leuschel:
Model checking object petri nets in prolog. PPDP 2004: 20-31 - [c44]Manoranjan Satpathy, Michael Leuschel, Michael J. Butler
:
ProTest: An Automatic Test Environment for B Specifications. MBT 2004: 113-136 - 2003
- [c43]Juan Carlos Augusto, Carla Ferreira
, Andrew M. Gravell, Michael Leuschel, Karen M. Y. Ng:
The Benefits of Rapid Modelling for E-business System Development. ER (Workshops) 2003: 17-28 - [c42]Stephen-John Craig, Michael Leuschel:
A Compiler Generator for Constraint Logic Programs. Ershov Memorial Conference 2003: 148-161 - [c41]Michael Leuschel, Michael J. Butler:
ProB: A Model Checker for B. FME 2003: 855-874 - [c40]Daniel Elphick, Michael Leuschel, Simon J. Cox:
Partial Evaluation of MATLAB. GPCE 2003: 344-363 - [c39]Helko Lehmann, Michael Leuschel:
Inductive Theorem Proving by Program Specialisation: Generating Proofs for Isabelle Using Ecce. LOPSTR 2003: 1-19 - [c38]Juan Carlos Augusto, Yvonne Howard, Andrew M. Gravell, Carla Ferreira
, Stefan Gruner, Michael Leuschel:
Model-Based Approaches for Validating Business Critical Systems. STEP 2003: 225-233 - 2002
- [c37]Michael Leuschel:
Homeomorphic Embedding for Online Termination of Symbolic Methods. The Essence of Computation 2002: 379-403 - 2001
- [c36]Michael Leuschel, Thierry Massart, Andrew Currie:
How to Make FDR Spin LTL Model Checking of CSP by Refinement. FME 2001: 99-118 - [c35]Michael Leuschel, Stefan Gruner:
Abstract Conjunctive Partial Deduction Using Regular Types and Its Application to Model Checking. LOPSTR 2001: 91-110 - [c34]Michael Leuschel:
Design and Implementation of the High-Level Specification Language CSP(LP) in Prolog. PADL 2001: 14-28 - 2000
- [c33]Michael Leuschel, Helko Lehmann:
Coverability of Reset Petri Nets and Other Well-Structured Transition Systems by Partial Deduction. Computational Logic 2000: 101-115 - [c32]Helko Lehmann, Michael Leuschel:
Decidability Results for the Propositional Fluent Calculus. Computational Logic 2000: 762-776 - [c31]Helko Lehmann, Michael Leuschel:
Solving Planning Problems by Partial Deduction. LPAR 2000: 451-468 - [c30]Michael Leuschel, Helko Lehmann:
Solving coverability problems of petri nets by partial deduction. PPDP 2000: 268-279 - 1999
- [c29]Robert Glück, Michael Leuschel:
Abstraction-Based Partial Deduction for Solving Inverse Problems - A Transformational Approach to Software Verification. Ershov Memorial Conference 1999: 93-100 - [c28]Jonathan C. Martin, Michael Leuschel:
Sonic Partial Deduction. Ershov Memorial Conference 1999: 101-112 - [c27]Michael Leuschel, Thierry Massart:
Infinite State Model Checking by Abstract Interpretation and Program Specialisation. LOPSTR 1999: 62-81 - [c26]Michael Leuschel:
Preface - Workshop on Optimization and Implementation of Declarative Programs. WOID@ICLP 1999: 127-128 - [c25]Michael Leuschel, Jesper Jørgensen:
Efficient Specialisation in Prolog Using the Hand-Written Compiler Generator LOGEN. WOID@ICLP 1999: 157-162 - 1998
- [c24]Maurice Bruynooghe, Michael Leuschel, Konstantinos Sagonas
:
A Polyvariant Binding-Time Analysis for Off-line Partial Deduction. ESOP 1998: 27-41 - [c23]Michael Leuschel:
Program Specialisation and Abstract Interpretation Reconciled. IJCSLP 1998: 220-234 - [c22]Michael Leuschel:
Improving Homeomorphic Embedding for Online Termination. LOPSTR 1998: 199-218 - [c21]Michael Leuschel:
Logic Program Specialisation. Partial Evaluation 1998: 155-188 - [c20]Michael Leuschel:
Advanced Logic Program Specialisation. Partial Evaluation 1998: 271-292 - [c19]Michael Leuschel:
On the Power of Homeomorphic Embedding for Online Termination. SAS 1998: 230-245 - 1997
- [c18]Stefaan Decorte, Danny De Schreye
, Michael Leuschel, Bern Martens, Konstantinos Sagonas
:
Termination Analysis for Tabled Logic Programming. LOPSTR 1997: 111-127 - [c17]Michael Leuschel, Bern Martens, Konstantinos Sagonas
:
Preserving Termination of Tabled Logic Programs While Unfolding. LOPSTR 1997: 189-205 - [c16]Michael Leuschel:
Specialization of Declarative Programs and Its Applications (Workshop Overview). ILPS 1997: 413-414 - [c15]Michael Leuschel:
Extending Homeomorphic Embedding in the Context of Logic Programming. WLP 1997 - [c14]Michael Leuschel, Danny De Schreye:
Constrained Partial Deduction. WLP 1997 - 1996
- [c13]Jesper Jørgensen, Michael Leuschel:
Efficiently Generating Efficient Generating Extensions in Prolog. Dagstuhl Seminar on Partial Evaluation 1996: 238-262 - [c12]Michael Leuschel, Bern Martens:
Global Control for Partial Deduction through Characteristic Atoms and Global Trees. Dagstuhl Seminar on Partial Evaluation 1996: 263-283 - [c11]Michael Leuschel, Danny De Schreye, D. Andre de Waal:
A Conceptual Embedding of Folding into Partial Deduction: Towards a Maximal Integration. JICSLP 1996: 319-332 - [c10]Michael Leuschel, Danny De Schreye
:
Logic Program Specialisation: How to Be More Specific (Abstract). LOPSTR 1996: 58 - [c9]Jesper Jørgensen, Michael Leuschel, Bern Martens:
Conjunctive Partial Deduction in Practice. LOPSTR 1996: 59-82 - [c8]Michael Leuschel, Morten Heine Sørensen:
Redundant Argument Filtering of Logic Programs. LOPSTR 1996: 83-103 - [c7]Michael Leuschel, Danny De Schreye
:
Logic Program Specialisation: How To Be More Specific. PLILP 1996: 137-151 - 1995
- [c6]Michael Leuschel, Bern Martens:
Generating Specialised Update Procedures Through Partial Deduction of the Ground Representation. Deductive Databases / Abduction in Deductive Databases 1995: 81-95 - [c5]Michael Leuschel:
Ecological Partial Deduction: Preserving Characteristic Trees Without Constraints. LOPSTR 1995: 1-16 - [c4]Michael Leuschel, Danny De Schreye
:
Towards Creating Specialised Integrity Checks through Partial Evaluation of Meta-Interpreters. PEPM 1995: 253-263 - [c3]Michael Leuschel, Bern Martens:
Partial Deduction of the Ground Representation and its Application to Integrity Checking. ILPS 1995: 495-509 - [c2]Danny De Schreye, Michael Leuschel, Bern Martens:
Tutorial on Program Specialisation (Abstract). ILPS 1995: 615-616 - 1994
- [c1]Michael Leuschel:
Partial Evaluation of the "Real Thing". LOPSTR 1994: 122-137
Parts in Books or Collections
- 2023
- [p5]Michael Leuschel
:
ProB: Harnessing the Power of Prolog to Bring Formal Models and Mathematics to Life. Prolog: The Next 50 Years 2023: 239-247 - 2019
- [p4]Fabrice Kordon, Michael Leuschel, Jaco van de Pol, Yann Thierry-Mieg:
Software Architecture of Modern Model Checkers. Computing and Software Science 2019: 393-419 - 2013
- [p3]Jérôme Falampin, Hung Le-Dang, Michael Leuschel, Mikael Mokrani, Daniel Plagge:
Improving Railway Data Validation with ProB. Industrial Deployment of System Engineering Methods 2013: 27-43 - 2004
- [p2]Wim Vanhoof, Maurice Bruynooghe, Michael Leuschel:
Binding-Time Analysis for Mercury. Program Development in Computational Logic 2004: 189-232 - [p1]Michael Leuschel, Stephen-John Craig, Maurice Bruynooghe, Wim Vanhoof:
Specialising Interpreters Using Offline Partial Deduction. Program Development in Computational Logic 2004: 340-375
Editorship
- 2024
- [e8]Silvia Bonfanti
, Angelo Gargantini
, Michael Leuschel
, Elvinia Riccobene
, Patrizia Scandurra
:
Rigorous State-Based Methods - 10th International Conference, ABZ 2024, Bergamo, Italy, June 25-28, 2024, Proceedings. Lecture Notes in Computer Science 14759, Springer 2024, ISBN 978-3-031-63789-6 [contents] - 2012
- [e7]John Derrick
, John S. Fitzgerald, Stefania Gnesi
, Sarfraz Khurshid, Michael Leuschel, Steve Reeves
, Elvinia Riccobene
:
Abstract State Machines, Alloy, B, VDM, and Z - Third International Conference, ABZ 2012, Pisa, Italy, June 18-21, 2012. Proceedings. Lecture Notes in Computer Science 7316, Springer 2012, ISBN 978-3-642-30884-0 [contents] - 2010
- [e6]Frank S. de Boer, Marcello M. Bonsangue, Stefan Hallerstede, Michael Leuschel:
Formal Methods for Components and Objects - 8th International Symposium, FMCO 2009, Eindhoven, The Netherlands, November 4-6, 2009. Revised Selected Papers. Lecture Notes in Computer Science 6286, Springer 2010, ISBN 978-3-642-17070-6 [contents] - 2009
- [e5]Michael Leuschel, Heike Wehrheim:
Integrated Formal Methods, 7th International Conference, IFM 2009, Düsseldorf, Germany, February 16-19, 2009. Proceedings. Lecture Notes in Computer Science 5423, Springer 2009, ISBN 978-3-642-00254-0 [contents] - 2007
- [e4]Michael Leuschel, Andreas Podelski:
Proceedings of the 9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, July 14-16, 2007, Wroclaw, Poland. ACM 2007, ISBN 978-1-59593-769-8 [contents] - 2003
- [e3]Michael Leuschel:
Logic Based Program Synthesis and Tranformation, 12th International Workshop, LOPSTR 2002, Madrid, Spain, September 17-20,2002, Revised Selected Papers. Lecture Notes in Computer Science 2664, Springer 2003, ISBN 3-540-40438-4 [contents] - [e2]Michael Leuschel:
Proceedings of the 2003 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, 2003, San Diego, California, USA, June 7, 2003. ACM 2003, ISBN 1-58113-667-6 [contents] - 1999
- [e1]Michael Leuschel:
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. Electronic Notes in Theoretical Computer Science 30(2), Elsevier 1999 [contents]
Informal and Other Publications
- 2022
- [i18]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:
50 Years of Prolog and Beyond. CoRR abs/2201.10816 (2022) - [i17]David Geleßus, Michael Leuschel:
Making ProB compatible with SWI-Prolog. CoRR abs/2205.04373 (2022) - [i16]Sebastian Stock, Fabian Vu, Atif Mashkoor, Michael Leuschel, Alexander Egyed:
IVOIRE Deliverable 1.1: Classification of existing VOs & tools and Formalization of VOs semantics. CoRR abs/2205.06138 (2022) - [i15]Sebastian Stock, Fabian Vu, David Geleßus, Atif Mashkoor, Michael Leuschel, Alexander Egyed:
Formalization of Advanced VOs semantics and VO Refinement. CoRR abs/2205.08988 (2022) - [i14]Sebastian Stock, Atif Mashkoor, Michael Leuschel, Alexander Egyed:
Trace Refinement in B and Event-B. CoRR abs/2207.14043 (2022) - 2021
- [i13]Atif Mashkoor, Michael Leuschel, Alexander Egyed:
Validation Obligations: A Novel Approach to Check Compliance between Requirements and their Formal Specification. CoRR abs/2102.06037 (2021) - 2020
- [i12]Philipp Körner
, David Schneider, Michael Leuschel:
On the Performance of Bytecode Interpreters in Prolog. CoRR abs/2008.12543 (2020) - 2016
- [i11]Jens Bendisposto, Philipp Koerner, Michael Leuschel, Jeroen Meijer, Jaco van de Pol, Helen Treharne, Jorden Whitefield:
Symbolic Reachability Analysis of B through ProB and LTSmin. CoRR abs/1603.04401 (2016) - [i10]Matthias van der Hallen, Sergey Paramonov, Michael Leuschel, Gerda Janssens:
Knowledge Representation Analysis of Graph Mining. CoRR abs/1608.08956 (2016) - 2013
- [i9]Uwe Glässer, Stefan Hallerstede, Michael Leuschel, Elvinia Riccobene:
Integration of Tools for Rigorous Software Construction and Analysis (Dagstuhl Seminar 13372). Dagstuhl Reports 3(9): 74-105 (2013) - 2012
- [i8]Thierry Lecomte
, Lilian Burdy, Michael Leuschel:
Formally Checking Large Data Sets in the Railways. CoRR abs/1210.6815 (2012) - 2011
- [i7]Stefan Hallerstede, Michael Leuschel:
Constraint-Based Deadlock Checking of High-Level Specifications. CoRR abs/1109.2015 (2011) - 2009
- [i6]Michael Leuschel, Salvador Tamarit, Germán Vidal:
Improving Size-Change Analysis in Offline Partial Evaluation. CoRR abs/0903.2202 (2009) - [i5]Jens Bendisposto, Ian Endrijautzki, Michael Leuschel, David Schneider:
A Semantics-Aware Editing Environment for Prolog in Eclipse. CoRR abs/0903.2252 (2009) - 2007
- [i4]Michael Leuschel, Jens Bendisposto:
Animating and Model Checking B Specifications with Higher-Order Recursive Functions. Rigorous Methods for Software Construction and Analysis 2007 - 2002
- [i3]Michael Leuschel, Maurice Bruynooghe:
Logic program specialisation through partial deduction: Control issues. CoRR cs.PL/0202012 (2002) - [i2]Michael Leuschel, Jesper Jørgensen, Wim Vanhoof, Maurice Bruynooghe:
Offline Specialisation in Prolog Using a Hand-Written Compiler Generator. CoRR cs.PL/0208009 (2002) - 2000
- [i1]Maurice Bruynooghe, Michael Leuschel, Konstantinos Sagonas:
A Polyvariant Binding-Time Analysis for Off-line Partial Deduction. CoRR cs.PL/0003068 (2000)
Coauthor Index
![](https://dblp.uni-trier.de/img/cog.dark.24x24.png)
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-06-29 00:48 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint