ToC

2022

  • Joshua Schmidt, Michael Leuschel
    SMT solving for the validation of B and Event-B models.
    In Software Tools for Technology Transfer (STTT), Springer-Verlag, 2022.

    2016

    • Ivaylo Dobrikov, Michael Leuschel
      Enabling Analysis for Event-B (Technical Report).
      Technical Report, Institut für Informatik, University of Düsseldorf, STUPS/2016/xx, 2016.
    • Michael Leuschel
      Formal Model-Based Constraint Solving and Document Generation.
      In SBMF'2016, Lecture Notes in Computer Science, Springer, 2016.

    2015

    • Ladenberger, Lukas, Hansen, Dominik, Wiegard, Harald, Bendisposto, Jens, Leuschel, Michael
      Validation of the ABZ landing gear system using ProB.
      In International Journal on Software Tools for Technology Transfer, Springer Berlin Heidelberg, 1-17, 2015.
    • David Schneider, Michael Leuschel, Tobias Witt
      Model-Based Problem Solving for University Timetable Validation and Improvement.
      In FM 2015: Formal Methods: 20th International Symposium, Lecture Notes in Computer Science (Book 9109), Springer, 487-495, 2015.
      • Sebastian Krings, Jens Bendisposto, Michael Leuschel
        From Failure to Proof: The ProB Disprover for B and Event-B.
        In Proceedings SEFM'2015, LNCS 9276, Springer, 2015.
      • Sebastian Krings, Michael Leuschel
        Inferring Physical Units in Formal Models.
        In Software & Systems Modeling, Springer Berlin Heidelberg, 1-23, 2015.

      2014

      • Lukas Ladenberger, Ivaylo Dobrikov, Michael Leuschel
        An Approach for Creating Domain Specific Visualisations of CSP Models.
        In HOFM 2014, Dimitra Giannakopoulou and Gwen Salaün, LNCS, 2014.
      • Ivaylo Dobrikov, Michael Leuschel
        Optimising the ProB Model Checker for B using Partial Order Reduction.
        In SEFM 2014, Dimitra Giannakopoulou and Gwen Salaün, LNCS 8702, 220--234, 2014.
      • Michael Leuschel, Jens Bendisposto, Ivaylo Dobrikov, Sebastian Krings, Daniel Plagge
        From Animation to Data Validation: The ProB Constraint Solver 10 Years On.
        In Formal Methods Applied to Complex Systems: Implementation of the B Method, Jean-Louis Boulanger, Wiley ISTE, 427--446, 2014.
      • Ivaylo Dobrikov, Michael Leuschel
        Optimising the ProB Model Checker for B using Partial Order Reduction.
        Technical Report, Institut für Informatik, Heinrich-Heine-Universität Düsseldorf, STUPS/2014/xx, 2014.
      • Sebastian Krings, Jens Bendisposto, Michael Leuschel
        Turning Failure into Proof: Evaluating the ProB Disprover.
        In Proceedings of the 1st International Workshop about Sets and Tools, 2014.
      • John Witulski, Michael Leuschel
        Checking Computations of Formal Method Tools - A Secondary Toolchain for ProB.
        In Proceedings of the 1st Workshop on Formal-IDE, EPTCS, 149, Electronic Proceedings in Theoretical Computer Science, 2014.
      • Jens Bendisposto, Sebastian Krings, Michael Leuschel
        Who watches the watchers: Validating the ProB Validation Tool.
        In Proceedings of the 1st Workshop on Formal-IDE, EPTCS, 149, Electronic Proceedings in Theoretical Computer Science, 2014.
      • Dominik Hansen, Lukas Ladenberger, Harald Wiegard, Jens Bendisposto, Michael Leuschel
        Validation of the ABZ Landing Gear System using ProB.
        In ABZ 2014: The Landing Gear Case Study, 2014.
      • Dominik Hansen, Jens Bendisposto, Michael Leuschel
        Integrating ProB into the TLA Toolbox.
        In TLA Workshop, 2014.
      • Dominik Hansen, Michael Leuschel
        Translating B to TLA + for Validation with TLC.
        In Proceedings ABZ'14, LNCS 8477, 40--55, 2014.
      • Michael Leuschel, David Schneider
        Towards B as a High-Level Constraint Modelling Language.
        In Abstract State Machines, Alloy, B, TLA, VDM, and Z, Ait Ameur, Yamine and Schewe, Klaus-Dieter, Lecture Notes in Computer Science, 8477, Springer Berlin Heidelberg, 101-116, 2014.
      • Michael Leuschel
        Towards Constraint-Solving over Higher-Order Unbounded Datatypes using Formal Methods Tools.
        In VPT 2014, Alexei Lisitsa and Andrei Nemytykh, EPiC Series, 28, EasyChair, 1-1, 2014.

      2013

      2012

      • Thierry Lecomte, Lilian Burdy, Michael Leuschel
        Formally Checking Large Data Sets in the Railways.
        In CoRR, abs/1210.6815, 2012.
      • Dominik Hansen, Michael Leuschel
        Translating TLA+ to B for Validation with ProB.
        In Proceedings iFM'2012, LNCS 7321, Springer, 24--38, 2012.
      • Daniel Plagge, Michael Leuschel
        Validating B, Z and TLA+ using ProB and Kodkod.
        In Proceedings FM'2012, Dimitra Giannakopoulou and Dominique Méry, LNCS 7436, Springer, 372--386, 2012.

      2011

      • Michael Leuschel, Jérôme Falampin, Fabian Fritz, Daniel Plagge
        Automated Property Verification for Large Scale B Models with ProB.
        In Formal Aspects of Computing, 23, 6, 683--709, 2011.
      • Jens Bendisposto, Michael Leuschel
        Automatic Flow Analysis for Event-B.
        In Proceedings of Fundamental Approaches to Software Engineering (FASE) 2011, Dimitra Giannakopoulou and Fernando Orejas, Lecture Notes in Computer Science, 6603, Springer, 50--64, 2011.
      • Stefan Hallerstede, Michael Leuschel
        Constraint-Based Deadlock Checking of High-Level Specifications.
        In Theory and Practice of Logic Programming, 11, 4--5, Cambridge University Press, 767--782, 2011.
      • Stefan Hallerstede, Michael Leuschel
        Finding Deadlocks of Event-B Models by Constraint Solving.
        In B2011 Workshop (short paper), 2011.
      • Rainer Gmehlich, Katrin Grau, Stefan Hallerstede, Michael Leuschel, Felix Lösch, Daniel Plagge
        On Fitting a Formal Method into Practice.
        In Proceedings ICFEM'2011, Shengchao Qin and Zongyan Qiu, Lecture Notes in Computer Science, 6991, Springer, 195--210, 2011.

      2010

      • Stefan Hallerstede, Michael Leuschel, Daniel Plagge
        Refinement-Animation for Event-B - Towards a Method of Validation.
        In Proceedings ABZ'2010, Lecture Notes in Computer Science, 5977, Springer-Verlag, 287--301, 2010.
      • Edd Turner, Michael Butler, Michael Leuschel
        A Refinement-Based Correctness Proof of Symmetry Reduced Model Checking.
        In Proceedings ABZ'2010, Lecture Notes in Computer Science, 5977, Springer-Verlag, 231--244, 2010.
      • Daniel Plagge, Michael Leuschel
        Seven at one stroke: LTL model checking for High-level Specifications in B, Z, CSP, and more.
        In Software Tools for Technology Transfer (STTT), 12, 1, Springer-Verlag, 9--21, 2010.
      • Michael Leuschel, Thierry Massart
        Efficient Approximate Verification of B via Symmetry Markers.
        In Annals of Mathematics and Artificial Intelligence, 59, 1, 81--106, 2010.
      • Michael Leuschel, Jens Bendisposto
        Directed Model Checking for B: An Evaluation and New Techniques.
        In SBMF'2010, Jim Davies and Leila Silva and Adenilso da Silva Simão, Lecture Notes in Computer Science, 6527, Springer, 1--16, 2010.

      2009

      • Michael Leuschel, Dominique Cansell, Michael Butler
        Validating and Animating Higher-Order Recursive Functions in B.
        In Festschrift for Egon Börger, Jean-Raymond Abrial and Uwe Glässer, Lecture Notes in Computer Science, 5115, Springer-Verlag, 2009.
      • Michael Leuschel, Jérôme Falampin, Fabian Fritz, Daniel Plagge
        Automated Property Verification for Large Scale B Models.
        In Proceedings FM 2009, Lecture Notes in Computer Science, 5850, Springer-Verlag, 708--723, 2009.
      • Daniel Plagge, Michael Leuschel, Ilya Lopatkin, Alexander Romanovsky
        SAL, Kodkod, and BDDs for Validation of B Models. Lessons and Outlook.
        In Proceedings AFM 2009, 16--22, 2009.
      • Jens Bendisposto, Michael Leuschel
        Proof Assisted Model Checking for B.
        In Proceedings of ICFEM 2009, Karin Breitman and Ana Cavalcanti, Lecture Notes in Computer Science, 5885, Springer, 504-520, 2009.
      • 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.
        In Proceedings TESTCOM/FATES 2009, Lecture Notes in Computer Science, 5826, Springer-Verlag, 179--194, 2009.
      • Lukas Ladenberger, Jens Bendisposto, Michael Leuschel
        Visualising Event-B Models with B-Motion Studio.
        In Proceedings of FMICS 2009, Marı́a Alpuente and Byron Cook and Christophe Joubert, Lecture Notes in Computer Science, 5825, Springer, 202-204, 2009.

      2008

      • Michael Leuschel, Michael Butler
        ProB: An Automated Analysis Toolset for the B Method.
        In Software Tools for Technology Transfer (STTT), 10, 2, Springer-Verlag, 185--203, 2008.
      • Corinna Spermann, Michael Leuschel
        ProB gets Nauty: Effective Symmetry Reduction for B and Z Models.
        In Proceedings TASE 2008, IEEE, 15--22, 2008.

      2005

      • Michael Leuschel, Michael Butler
        Combining CSP and B for Specification and Property Verification.
        In FM'2005, John Fitzgerald and Ian Hayes and Andrzej Tarlecki, Lecture Notes in Computer Science, 3582, Springer-Verlag, 221--236, 2005.
      • Michael Leuschel, Michael Butler
        Automatic Refinement Checking for B.
        In Proceedings ICFEM, Kung-Kiu Lau and Richard Banach, Lecture Notes in Computer Science, 3785, Springer-Verlag, 345--359, 2005.

      2003

      • Michael Leuschel, Michael Butler
        ProB: A Model Checker for B.
        In FME, Araki Keijiro and Stefania Gnesi and Mandrio Dino, Lecture Notes in Computer Science, 2805, Springer-Verlag, 855--874, 2003.