default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDMichael Leuschel
Person information
- affiliation: University of Düsseldorf, Germany
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 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) - [c168]Michael Leuschel:
B2SAT: A Bare-Metal Reduction of B to SAT. FM (2) 2024: 122-139 - [c167]Jan Gruteser, Michael Leuschel:
Validation of RailML Using ProB. ICECCS 2024: 245-256 - [c166]Jan Roßbach, Oliver De Candido, Ahmed Hammam, Michael Leuschel:
Evaluating AI-Based Components in Autonomous Railway Systems - A Methodology. KI 2024: 190-203 - [c165]Fabian Vu, Jannik Dunkelau, Michael Leuschel:
Validation of Reinforcement Learning Agents and Safety Shields with ProB. NFM 2024: 279-297 - [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] - 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 - [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 - 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) - [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 - [d3]Michael Leuschel:
ProB Operation Caching ifm2022 Artefact. Zenodo, 2022
- [d2]Michael Leuschel:
ProB Linux 1.12.0-beta1. Zenodo, 2022 - [d1]Michael Leuschel:
ProB Operation Caching ifm2022 Artefact. Zenodo, 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
- [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) - [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 - [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
- [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) - [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 - [i12]Philipp Körner, David Schneider, Michael Leuschel:
On the Performance of Bytecode Interpreters in Prolog. CoRR abs/2008.12543 (2020)
2010 – 2019
- 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 - [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 - 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) - [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
- [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) - [c123]Sebastian Krings, Michael Leuschel:
Constraint Logic Programming over Infinite Domains with an Application to Proof. WLP / WFLP 2017: 73-87 - 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) - [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 - [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) - 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
- [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) - [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
- [j30]Stefan Hallerstede, Michael Leuschel, Daniel Plagge:
Validation of formal models by refinement animation. Sci. Comput. Program. 78(3): 272-292 (2013) - [c99]Sebastian Krings, Michael Leuschel:
Inferring Physical Units in B Models. SEFM 2013: 137-151 - [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 - [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
- [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) - [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 - [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] - [i8]Thierry Lecomte, Lilian Burdy, Michael Leuschel:
Formally Checking Large Data Sets in the Railways. CoRR abs/1210.6815 (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) - [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.