Jump to contentJump to search

Michael Leuschel

Contact Information

Heinrich-Heine-Universität Düsseldorf

Institut für Informatik

Universitätsstraße 1
D-40225 Düsseldorf

 

Email: 

Phone: +49 (211) 81-10710
Fax: +49 (211) 81-10712

Room: 25.12.02.60

 

Academic Activities

Current Courses (Winterterm 2016)

You can find proposed theses undefinedhere.

Publications

2023

2022

  • Fabian Vu, Christopher Happe, Michael Leuschel
    Generating Domain-Specific Interactive Validation Documents.
    In Proceedings FMICS, LNCS, 13487, Springer, 32--49, 2022.
  • Fabian Vu, Dominik Brandt, Michael Leuschel
    Model Checking B Models via High-Level Code Generation.
    In Proceedings ICFEM, LNCS, 13478, Springer, 334--351, 2022.
  • Sophia Reinhardt, Joshua Schmidt, Jonas Schneider, Michael Leuschel, Christiane Schüle, Jörg Schipper
    VertiGo-App - Smartphone-based video nystagmography using artificial intelligence.
    In Laryngorhinootologie 2022, 101, 2, 243--244, 2022.
  • SMT solving for the validation of B and Event-B models.
    In Software Tools for Technology Transfer (STTT), Springer-Verlag, 2022.

    2021

    2020

    2019

    2018

    2016

    • Constraint Logic Programming over Infinite Domains with an Application to Proof.
      In Proceedings of the 30th Workshop on (Constraint) Logic Programming, EPTCS, 234, 2016.
    • Ivaylo Dobrikov, Michael Leuschel
      Optimising the ProB Model Checker for B using partial order reduction.
      In Formal Aspects of Computing, 28, 2, 179--323, 2016.
    • Proof Assisted Symbolic Model Checking for B and Event-B.
      In Proceedings ABZ 2016, LNCS, 9675, Springer, 2016.
    • Interactive Model Repair by Synthesis.
      In Proceedings ABZ 2016, LNCS, 9675, Springer, 2016.
    • SMT Solvers for Validation of B and Event-B models.
      In Proceedings iFM 2016, LNCS, 9681, Springer, 2016.
    • Jens Bendisposto, Philipp Körner, Michael Leuschel, Jeroen Meijer, van de Pol, Jaco, Helen Treharne, Jorden Whitefield
      Symbolic Reachability Analysis of B through ProB and LTSmin.
      In Proceedings iFM 2016, LNCS, 9681, Springer, 2016.
    • Ivaylo Dobrikov, Michael Leuschel
      Enabling Analysis for Event-B.
      In Proceedings ABZ 2016, LNCS, 9675, Springer, 2016.
    • Using B and ProB for Data Validation Projects.
      In Proceedings ABZ 2016, LNCS, 9675, Springer-Verlag, 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.
      • Ivaylo Dobrikov, Daniel Plagge,, Michael Leuschel
        LTL Model Checking under Fairness in ProB.
        In Proceedings SEFM'16, LNCS, 9763, Springer, 2016.
      • Lukas Ladenberger, Michael Leuschel
        BMotionWeb: A Tool for Rapid Creation of Formal Prototypes.
        In Proceedings SEFM'16, LNCS, 9763, Springer, 2016.
        • Formal Model-Based Constraint Solving and Document Generation.
          In SBMF'2016, Lecture Notes in Computer Science, Springer, 2016.
        • Joy Clark, Jens Bendisposto, Stefan Hallerstede, Dominik Hansen, Michael Leuschel
          Generating Event-B Specifications from Algorithm Descriptions.
          In Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings, Michael J. Butler and Klaus-Dieter Schewe and Atif Mashkoor and Miklós Biró, Lecture Notes in Computer Science, 9675, Springer, 183--197, 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.
        • 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.
          • Evaluating Interpreter Design in Prolog.
            In 18. Kolloquium Programmiersprachen und Grundlagen der Programmierung KPS 2015, Schriftenreihe des Instituts für Computersprachen, Springer, 2015.
          • From Failure to Proof: The ProB Disprover for B and Event-B.
            In Proceedings SEFM'2015, LNCS 9276, Springer, 2015.
          • Inferring Physical Units in Formal Models.
            In Software & Systems Modeling, Springer Berlin Heidelberg, 1-23, 2015.
          • Translating B to TLA+ for Validation with TLC.
            Technical Report, Institut für Informatik, Heinrich-Heine-Universität Düsseldorf, STUPS/2015/Feb, 2015.
          • Lukas Ladenberger, Michael Leuschel
            Mastering the Visualization of Larger State Spaces with Projection Diagrams.
            Technical Report, Institut für Informatik, Heinrich-Heine-Universität Düsseldorf, STUPS/2015/May, 2015.
          • Lukas Ladenberger, Michael Leuschel
            Mastering the Visualization of Larger State Spaces with Projection Diagrams.
            In Proceedings ICFEM'2015, LNCS 9407, Springer-Verlag, 153--169, 2015.

            2014

            • Michael Leuschel, Germán Vidal
              Fast offline partial evaluation of logic programs.
              In Information and Computation, 235, 70--97, 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.
            • 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.
            • 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.
            • Integrating ProB into the TLA Toolbox.
              In TLA Workshop, 2014.
            • Translating B to TLA + for Validation with TLC.
              In Proceedings ABZ'14, LNCS 8477, 40--55, 2014.
            • 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.
            • 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.
            • 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.
            • Bendisposto, Jens, Fritz, Fabian, Jastram, Michael, Leuschel, Michael, Weigelt, Ingo
              Developing Camille, a text editor for Rodin.
              In Software: Practice and Experience, 41, 2, John Wiley & Sons, Ltd., 189--198, 2011.
            • 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.
            • Carl Friedrich Bolz, Antonio Cuni, Maciej Fijałkowski, Michael Leuschel, Samuele Pedroni, Armin Rigo
              Allocation removal by partial evaluation in a tracing JIT.
              In PEPM, 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.
            • Carl Friedrich Bolz, Antonio Cuni, Maciej Fijałkowski, Michael Leuschel, Samuele Pedroni, Armin Rigo
              Runtime Feedback in a Meta-Tracing JIT for Efficient Dynamic Languages.
              In Proceedings of the 6th workshop on the Implementation, Compilation, Optimization of Object-Oriented Languages and Programming Systems, ICOOOLPS '11, 2011.

            2010

            • Michael Leuschel, Salvador Tamarit, Germán Vidal
              Fast and Accurate Strong Termination Analysis with an Application to Partial Evaluation.
              In Proceedings WFLP'2009, Santiago Escobar, LNCS 5979, Springer-Verlag, 111--127, 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.
            • Carl Friedrich Bolz, Michael Leuschel, David Schneider
              Towards a Jitting VM for Prolog Execution.
              In PPDP '10 - Proceedings of the 12th international ACM SIGPLAN symposium on Principles and practice of declarative programming, ACM, 2010.
            • David Schneider, Carl Friedrich Bolz, Michael Leuschel
              Jitting Prolog for Fun and Profit.
              In DYLA 2010 - 4th Workshop on Dynamic Languages and Applications, 2010.
            • 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.
            • GEPAVAS Gerichtete und parallele Validierung von abstrakten Spezifikationen - Projektreport.
              Technical Report, University of Düsseldorf, 2010.
            • Michael Jastram, Stefan Hallerstede, Michael Leuschel, Aryldo G Russo Jr
              An Approach of Requirements Tracing in Formal Refinement.
              In VSTTE, Lecture Notes in Computer Science, 6217, Springer, 97-111, 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.
            • Carl Friedrich Bolz, Michael Leuschel, Armin Rigo
              Towards Just-In-Time Partial Evaluation of Prolog.
              In Logic-Based Program Synthesis and Transformation, 19th International Symposium, LOPSTR 2009, Coimbra, Portugal, September 2009, Revised Selected Papers, Danny De Schreye, Lecture Notes in Computer Science, 6037, Springer, 158-172, 2009.
            • Michael Leuschel, Marisa Llorens, Javier Olivier, Josep Silva, Salvador Tamarit
              SOC: A Slicer for CSP Specifications.
              In PEPM 2009, ACM Press, 2009.
              • Mireille Samia, Michael Leuschel
                Pie Tree Visualization.
                In Proceedings SEKE, Knowledge Systems Institute, 400--405, 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.
                • 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.
                • 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.
                • Stefan Hallerstede, Michael Leuschel
                  How to explain mistakes.
                  In TFM 2009, Lecture Notes in Computer Science, Springer-Verlag, 105--124, 2009.
                • Mireille Samia, Harald Wiegard, Jens Bendisposto, Michael Leuschel
                  High-Level versus Low-Level Specifications: Comparing B with Promela and ProB with Spin.
                  In Proceedings TFM-B 2009, Attiogbe and Mery, APCB, 2009.
                • Parallel Model Checking of Event-B Specification with ProB.
                  In 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.
                  • Michael Leuschel, Mireille Samia, Jens Bendisposto, Li Luo
                    Easy Graphical Animation and Formula Viewing for Teaching B.
                    In The B Method: from Research to Teaching, C. Attiogbé and H. Habrias, Lina, 17--32, 2008.
                  • Corinna Spermann, Michael Leuschel
                    ProB gets Nauty: Effective Symmetry Reduction for B and Z Models.
                    In Proceedings TASE 2008, IEEE, 15--22, 2008.
                  • The High Road to Formal Validation: Model Checking High-Level versus Low-Level Specifications.
                    In ABZ 2008, Lecture Notes in Computer Science, 5238, Springer-Verlag, 4--23, 2008.
                  • Declarative Programming for Verification: Lessons and Outlook.
                    In Proceedings PPDP'2008, ACM Press, 1--7, 2008.
                  • Michael Leuschel, Germán Vidal
                    Fast Offline Partial Evaluation for Large Logic Programs.
                    In Proceedings LOPSTR'08, Michael Hanus, Lecture Notes in Computer Science, 5438, 119--134, 2008.
                  • Michael Leuschel, Marisa Llorens, Javier Olivier, Josep Silva, Salvador Tamarit
                    Static Slicing of CSP Specifications.
                    In Preproceedings LOPSTR'08, Michael Hanus, Lecture Notes in Computer Science, 5438, 103--118, 2008.
                  • Michael Leuschel, Marc Fontaine
                    Probing the Depths of CSP-M: A new FDR-compliant Validation Tool.
                    In ICFEM 2008, Springer-Verlag, 278--297, 2008.
                  • A Semantics-Aware Editing Environment for Prolog in Eclipse.
                    In Proceedings of the 18th Workshop on Logic-based methods in Programming Environments, WLPE, 2008.
                  • Jens Bendisposto, Michael Leuschel, O. Ligot, Mireille Samia
                    La validation de modèles Event-B avec le plug-in ProB pour RODIN.
                    In Technique et Science Informatiques, 27, 8, 1065-1084, 2008.
                    • Steve Barker, Michael Leuschel, Mauricio Varea
                      Efficient and Flexible Access Control via Jones-Optimal Logic Program Specialisation.
                      In Higher-Order and Symbolic Computation, 21, 1--2, 5--35, 2008.

                    2007

                    • Dragan Bosnacki, Alastair F. Donaldson, Michael Leuschel, Thierry Massart
                      Efficient Approximate Verification of Promela Models via Symmetry Markers.
                      In ATVA, Lecture Notes in Computer Science, 4762, Springer-Verlag, 300--315, 2007.
                    • BE4: The B Extensible Eclipse Editing Environment.
                      In Proceedings of B 2007, Jacques Julliand and Olga Kouchnarenko, Lecture Notes in Computer Science, 4355, Springer, 270-273, 2007.
                    • Karl Klose, Klaus Ostermann, Michael Leuschel
                      Partial Evaluation of Pointcuts.
                      In Practical Applications of Declarative Languages (PADL'07), Lecture Notes in Computer Science, Springer-Verlag, 320--334, 2007.
                    • A Generic Flash-Based Animation Engine for ProB.
                      In Proceedings of B 2007, Jacques Julliand and Olga Kouchnarenko, Lecture Notes in Computer Science, 4355, Springer, 266-269, 2007.
                    • Michael Leuschel, Michael Butler, Corinna Spermann, Edd Turner
                      Symmetry Reduction for B by Permutation Flooding.
                      In Proceedings B'2007, Lecture Notes in Computer Science, 4355, Springer-Verlag, 79--93, 2007.
                    • Michael Leuschel, Thierry Massart
                      Efficient Approximate Verification of B via Symmetry Markers.
                      In Proceedings International Symmetry Conference, 71--85, 2007.
                    • Manoranjan Satpathy, Michael Butler, Michael Leuschel, S. Ramesh
                      Automatic Testing from Formal Specifications.
                      In Tests and Proofs (TAP 2007), Lecture Notes in Computer Science, 4454, Springer-Verlag, 95--113, 2007.
                      • Edd Turner, Michael Leuschel, Corinna Spermann, Michael Butler
                        Symmetry Reduced Model Checking for B.
                        In Proceedings TASE 2007, IEEE, 25--34, 2007.
                      • Daniel Plagge, Michael Leuschel
                        Validating Z Specifications using the ProB Animator and Model Checker.
                        In Integrated Formal Methods, J. Davies and J. Gibbons, Lecture Notes in Computer Science, 4591, Springer-Verlag, 480--500, 2007.
                      • Debugging Event-B Models using the ProB Disprover Plug-in.
                        In Proceedings AFADL'07, 2007.
                      • Michael Leuschel, Daniel Plagge
                        Seven at one stroke: LTL model checking for High-level Specifications in B, Z, CSP, and more.
                        Technical Report, Institut für Informatik, Heinrich-Heine-Universität Düsseldorf, STUPS/2007/02, 2007.
                      • Michael Leuschel, Daniel Plagge
                        Seven at one stroke: LTL model checking for High-level Specifications in B, Z, CSP, and more.
                        In ISoLA, Yamine Aı̈t Ameur and Frédéric Boniol and Virginie Wiels, Revue des Nouvelles Technologies de l'Information, RNTI-SM-1, Cépaduès-Éditions, 73--84, 2007.

                        2006

                        • Michael Leuschel, Daniel Elphick, Mauricio Varea, Stephen Craig, Marc Fontaine
                          The Ecce and Logen Partial Evaluators and their Web Interfaces.
                          In Proceedings PEPM 06, John Hatcliff and Frank Tip, IBM Press, 88--94, 2006.
                        • Michael Leuschel, Stephen Craig, Daniel Elphick
                          Supervising Offline Partial Evaluation of Logic Programs using Online Techniques.
                          In Proceedings LOPSTR'06, German Puebla, Lecture Notes in Computer Science, 4407, Springer-Verlag, 43--59, 2006.
                        • Stephane Lo Presti, Michael Butler, Michael Leuschel, Chris Booth
                          Holistic Trust Design of E-Services.
                          In Trust in E-services: Technologies, Practices and Challenges, Ronggong Song and Larry Korba and George Yee, IGI Global, 113--139, 2006.
                          • Animating and Model Checking B Specifications with Higher-Order Recursive Functions.
                            In Dagstuhl Seminar 06191 "Rigorous Methods for Software Construction and Analysis", J. Abrial, U. Glässer, 2006.

                          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 Butler, Michael Leuschel, Colin Snook
                            Tools for system validation with B abstract machines.
                            In 12th International Workshop on Abstract State Machines, 57--69, 2005.
                          • Guest Editorial -- Special Issue on Automated Verification of Critical Systems.
                            In Formal Aspects of Computing, 17, 2, Springer-Verlag, 91-92, 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.
                            • Michael Leuschel, Stephen Craig
                              A Reconstruction of the Lloyd-Topor Transformation using Partial Evaluation.
                              In Pre-Proceedings of LOPSTR'05, Pat Hill, 2005.
                            • Michael Leuschel, Edd Turner
                              Visualising Larger State Spaces in ProB.
                              In ZB, Helen Treharne and Steve King and Martin Henson and Steve Schneider, Lecture Notes in Computer Science, 3455, Springer-Verlag, 6--23, 2005.
                            • Michael Leuschel, Germán Vidal
                              Forward Slicing by Conjunctive Partial Deduction and Argument Filtering.
                              In ESOP, Mooly Sagiv, Lecture Notes in Computer Science, 3444, Springer-Verlag, 61--76, 2005.
                            • Stephane Lo Presti, Michael Butler, Michael Leuschel, Chris Booth
                              A Trust Analysis Methodology for Pervasive Computing Systems.
                              In Trusting Agents for trusting Electronic Societies, R Falcone and S Barber and J Sabater and M Singh, Lecture Notes in Computer Science, 3577, Springer-Verlag, 2005.
                            • Manoranjan Satpathy, Michael Leuschel, Michael Butler
                              ProTest: An Automatic Test Environment for B Specifications.
                              In Electronic Notes in Theroretical Computer Science, 111, Elsevier, 113--136, 2005.
                            • Qian Wang, Gopal Gupta, Michael Leuschel
                              Towards Provably Correct Code Generation via Horn Logical Continuation Semantics.
                              In PADL, Manuel Hermengildo and Daniel Cabeza, Lecture Notes in Computer Science, 3350, Springer-Verlag, 98--112, 2005.
                            • Stephen Craig, Michael Leuschel
                              Self-Tuning Resource Aware Specialisation for Prolog.
                              In Proceedings PPDP'2005, ACM Press, 23--34, 2005.

                            2004

                            • Steve Barker, Michael Leuschel, Mauricio Varea
                              Efficient and Flexible Access Control via Logic Program Specialisation.
                              In PEPM, Nevin Heintze and Peter Sestoft, ACM Press, 190--119, 2004.
                            • Michael Butler, Michael Leuschel, Stephane Lo Presti, Phillip Turner
                              The Use of Formal Methods in the Analysis of Trust (Position Paper).
                              In iTrust, Christian Jensen and Stefan Poslad and Theo Dimitrakos, Lecture Notes in Computer Science, 2995, Springer-Verlag, 333--339, 2004.
                              • Stephen Craig, John Gallagher, Michael Leuschel, Kim S. Henriksen
                                Fully Automatic Binding Time Analysis for Prolog.
                                In LOPSTR, Sandro Etalle, Lecture Notes in Computer Science, 3573, Springer-Verlag, 53--68, 2004.
                              • Stephen Craig, Michael Leuschel
                                Lix: An Effective Self-applicable Partial Evaluator for Prolog.
                                In FLOPS, Yukiyoshi Kameyama and Peter J. Stuckey, Springer-Verlag, 85--99, 2004.
                              • A Framework for the Integration of Partial Evaluation and Abstract Interpretation of Logic Programs.
                                In ACM Transactions on Programming Languages and Systems (TOPLAS), 26, 3, ACM, 413--463, 2004.
                              • ProB: Un outil de modélisation formelle (Invited Talk).
                                In JFPLC, Fred Mesnard, Hermes Science Publications, Lavoisier, 13--13, 2004.
                              • Michael Leuschel, Stephen Craig, Maurice Bruynooghe, Wim Vanhoof
                                Specializing Interpreters using Offline Partial Deduction.
                                In Program Development in Computational Logic, Maurice Bruynooghe and Kung-Kiu Lau, Lecture Notes in Computer Science, 3049, Springer-Verlag, 341--376, 2004.
                              • Michael Leuschel, Jesper Jørgensen, Wim Vanhoof, Maurice Bruynooghe
                                Offline Specialisation in Prolog Using a Hand-Written Compiler Generator.
                                In TPLP, 4, 1--2, Cambridge University Press, 139--191, 2004.
                              • Michael Leuschel, Edd Turner
                                Visualising Larger State Spaces in ProB.
                                Technical Report, ECS, University of Southampton, 2004.
                                • Stephane Lo Presti, Michael Butler, Michael Leuschel, Colin Snook, Phillip Turner
                                  Formal Modelling and Verification of Trust in a Pervasive Application.
                                  Technical Report, DSSE, University of Southampton, 2004.
                                • Wim Vanhoof, Maurice Bruynooghe, Michael Leuschel
                                  Binding-Time Analysis for Mercury.
                                  In Program Development in Computational Logic, Maurice Bruynooghe and Kung-Kiu Lau, Lecture Notes in Computer Science, 3049, Springer-Verlag, 189--232, 2004.
                                • Berndt Farwer, Michael Leuschel
                                  Model Checking of Object Petri Nets in Prolog.
                                  In PPDP, Eugenio Moggi and David Scott Warren, ACM Press, 20--31, 2004.

                                2003

                                • Juan Carlos Augusto, Carla Ferreira, Andy M. Gravell, Michael Leuschel, Karen M.Y. Ng
                                  The Benefits of Rapid Modelling for E-Business System Development.
                                  In ER (Workshops), Manfred A. Jeusfeld and Oscar Pastor, Lecture Notes in Computer Science, 2814, Springer Verlag, 17--28, 2003.
                                • Juan Carlos Augusto, Michael Leuschel, Michael Butler, Carla Ferreira
                                  Using the Extensible Model Checker XTL to Verify StAC Business Specifications.
                                  In AVoCS, Michael Leuschel and Stefan Gruner and Stephane Lo Presti, 253--266, 2003.
                                • Michael Butler, Michael Leuschel, Stephane Lo Presti, David Allsopp, Patrick Beautement, Chris Booth, Mark Cusack, Mike Kirton
                                  Towards a Trust Analysis Framework for Pervasive Computing Scenarios.
                                  In IEEE Computing, 2, 3, 96, 2003.
                                • Stephen Craig, Michael Leuschel
                                  A Compiler Generator for Constraint Logic Programs.
                                  In Ershov Memorial Conference, M. Broy and A. Zamulin, Lecture Notes in Computer Science, 2890, Springer-Verlag, 2003.
                                • Daniel Elphick, Michael Leuschel, Simon J. Cox
                                  Partial Evaluation of MATLAB.
                                  In Generative Programming and Component Engineering, Second International Conference, GPCE 2003, Erfurt, Germany, September 22-25, 2003, Proceedings, 344--363, 2003.
                                • Helko Lehmann, Michael Leuschel
                                  Inductive Theorem Proving by Program Specialisation: Generating proofs for Isabelle using Ecce (Invited talk).
                                  In LOPSTR, Maurice Bruynooghe, Lecture Notes in Computer Science, 3018, Springer-Verlag, 1--19, 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.
                                • Michael Leuschel, Stephen Craig, Maurice Bruynooghe, Wim Vanhoof
                                  Specializing Interpreters using Offline Partial Deduction.
                                  Technical Report, ECS, University of Southampton, DSSE-TR-2003-5, 2003.
                                • Mauricio Varea, Michael Leuschel, Bashir Al-Hashimi
                                  Improving Compositional Verification of State-based Models by Reducing Modular Unbalance.
                                  In Refinement of Critical Systems, 2003.

                                2002

                                • Helko Lehmann, Michael Leuschel
                                  Generating inductive verification proofs for Isabelle using the partial evaluator Ecce.
                                  Technical Report, ECS, University of Southampton, DSSE-TR-2002-02, 2002.
                                  • Homeomorphic Embedding for Online Termination of Symbolic Methods.
                                    In The Essence of Computation -- Essays dedicated to Neil Jones, Torben Mogensen, David Schmidt, I. H. Sudborough, Lecture Notes in Computer Science, 2566, Springer-Verlag, 379--403, 2002.
                                  • Michael Leuschel, Maurice Bruynooghe
                                    Logic program specialisation through partial deduction: Control Issues.
                                    In Theory and Practice of Logic Programming, 2, 4--5, Cambridge University Press, 461--515, 2002.
                                  • Michael Leuschel, Stefan Gruner
                                    Abstract Conjunctive Partial Deduction using Regular Types and its Application to Model Checking.
                                    In LOPSTR, Alberto Pettorossi, Lecture Notes in Computer Science, 2372, Springer-Verlag, 91--110, 2002.
                                    • Michael Leuschel, Thierry Massart
                                      Logic programming and partial deduction for the verification of reactive systems: An experimental evaluation.
                                      In AVoCS, Gethin Norman and Martha Kwiatkowska and Dimitar Guelev, University of Birmingham, 143--149, 2002.
                                    • Mauricio Varea, Bashir Al-Hashimi, Michael Leuschel
                                      Finite and Infinite Model Checking of Dual Transition Petri Net Models.
                                      In AVoCS, 265--269, 2002.

                                    2001

                                    • Laksono Adhianto, Michael Leuschel
                                      Strategy for Improving Memory Locality Reuse and Exploiting Hidden Parallelism.
                                      In Proceedings of ISSM, 2001.
                                      • Hugh Glaser, Pieter H. Hartel, Michael Leuschel, Andrew Martin
                                        Declarative Languages in Education.
                                        In Encyclopaedia of Microcomputers, 27, Marcel Dekker Inc, 79--102, 2001.
                                      • Design and Implementation of the High-Level Specification Language CSP(LP).
                                        In PADL, Lecture Notes in Computer Science, 1990, Springer, 14--28, 2001.
                                      • Michael Leuschel, Laksono Adhianto, Michael Butler, Carla Ferreira, Leonid Mikhailov
                                        Animation and Model Checking of CSP and B using Prolog Technology.
                                        In Proceedings of the ACM Sigplan Workshop on Verification and Computational Logic, Michael Leuschel and Andreas Podelski and C.R. Ramakrishnan and Ulrich Ultes-Nitsche, 97--109, 2001.
                                        • Michael Leuschel, Thierry Massart, Andrew Currie
                                          How to make FDR Spin: LTL model checking of CSP using Refinement.
                                          In Proceedings FME'2001, J.N. Oliviera, P. Zave, Springer-Verlag, 99--118, 2001.
                                        • Michael Leuschel, Ivan Wolton, Thierry Massart, Laksono Adhianto
                                          Temporal Logic Model Checking of CSP: Tools and Techniques.
                                          In AVoCS 2001, David Nowak, Oxford University Computing Laboratory, 2001.

                                          2000

                                          • Andrew Currie, Michael Leuschel, Thierry Massart
                                            LTL Model Checking of CSP by Refinement: How to Make FDR Spin.
                                            In Proceedings VCL'2000, 2000.
                                            • Helko Lehmann, Michael Leuschel
                                              Decidability Results for the Propositional Fluent Calculus.
                                              In Computational Logic, John LLoyd, Lecture Notes in Computer Science, 1861, Springer-Verlag, 762--776, 2000.
                                              • Helko Lehmann, Michael Leuschel
                                                Solving Planning Problems by Partial Deduction.
                                                In LPAR, Michel Parigot and Andrei Voronkov, Lecture Notes in Computer Science, 1955, Springer-Verlag, 2000.
                                              • Michael Leuschel, Maurice Bruynooghe
                                                Control Issues in Partial Deduction: The Ever Ending Story.
                                                Technical Report, University of Southampton, 2000.
                                                • Michael Leuschel, Helko Lehmann
                                                  Coverability of Reset Petri Nets and other Well-Structured Transition Systems by Partial Deduction.
                                                  In Computational Logic, John Lloyd and Verónica Dahl and Ulrich Furbach and Manfred Kerber and Kung-Kiu Lau and Catuscia Palamidessi and Luı́s Moniz Pereira and Yehoshua Sagiv and Peter J. Stuckey, Lecture Notes in Computer Science, 1861, Springer-Verlag, 101--115, 2000.
                                                • Michael Leuschel, Helko Lehmann
                                                  Solving Coverability Problems of Petri Nets by Partial Deduction.
                                                  In PPDP, Maurizio Gabbrielli and Frank Pfenning, ACM Press, 268--279, 2000.

                                                1999

                                                • Danny De Schreye, Robert Glueck, Jesper Jørgensen, Michael Leuschel, Bern Martens, Morten H. Sørensen
                                                  Conjunctive Partial Deduction: Foundations, Control, Algorithms, and Experiments.
                                                  In Journal of Logic Programming, 41, 2--3, 231--277, 1999.
                                                • Robert Glueck, Michael Leuschel
                                                  Abstraction-Based Partial Deduction for Solving Inverse Problems -- A Transformational Approach to Software Verification.
                                                  In Ershov Memorial Conference, Lecture Notes in Computer Science, 1755, Springer-Verlag, 93--100, 1999.
                                                  • P. Hartel, Michael Butler, Andrew Currie, P. Henderson, Michael Leuschel, A. Martin, A. Smith, Ulrich Ultes-Nitsche, R.J. Walters
                                                    Questions and Answers About Ten Formal Methods.
                                                    In Proc. 4th Int. Workshop on Formal Methods for Industrial Critical Systems, S. Gnesi and D. Latella, STAR/CNR, Pisa, Italy, 179--203, 1999.
                                                    • Advanced Logic Program Specialisation.
                                                      In Partial Evaluation - Practice and Theory, DIKU 1998 International Summer School, Springer-Verlag, 271--292, 1999.
                                                    • Logic Program Specialisation.
                                                      In Partial Evaluation: Practice and Theory, John Hatcliff and Torben AE Mogensen and Peter Thiemann, Lecture Notes in Computer Science, 1706, Springer-Verlag, 155--188, 1999.
                                                    • Michael Leuschel, Jesper Jørgensen
                                                      Efficient Specialisation in Prolog Using the Hand-Written Compiler Generator LOGEN.
                                                      In Electronic Notes in Theoretical Computer Science, 30, 2, 157-162, 1999.
                                                      • Michael Leuschel, Jesper Jørgensen
                                                        Efficient Specialisation in Prolog Using a Hand-Written Compiler Generator.
                                                        Technical Report, University of Southampton, DSSE-TR-99-6, 1999.
                                                        • Michael Leuschel, Nick Linnenbruegger, Jerome Thoma
                                                          Analyzing Context-Free and Context-Sensitive Grammars by Abstract Interpretation.
                                                          In Proceedings of the Formal Grammar Conference FG'99, G-J. M. Kruijff and R. T. Oerle, University of Utrecht, 93--101, 1999.
                                                          • Michael Leuschel, Thierry Massart
                                                            Infinite State Model Checking by Abstract Interpretation and Program Specialisation.
                                                            In LOPSTR '99, A. Bossi, Lecture Notes in Computer Science, 1817, Springer-Verlag, 63--82, 1999.
                                                          • Jonathan C. Martin, Michael Leuschel
                                                            Sonic Partial Deduction.
                                                            In Ershov Memorial Conference, Lecture Notes in Computer Science, 1755, Springer-Verlag, 101--112, 1999.

                                                            1998

                                                            • Maurice Bruynooghe, Michael Leuschel, Konstantinos Sagonas
                                                              A Polyvariant Binding-Time Analysis for Off-line Partial Deduction.
                                                              In ESOP, C. Hankin, Lecture Notes in Computer Science, 1381, Springer-Verlag, 27--41, 1998.
                                                            • Stefaan Decorte, Danny De Schreye, Michael Leuschel, Bern Martens, Konstantinos Sagonas
                                                              Termination Analysis for Tabled Logic Programming.
                                                              In LOPSTR '97, N. Fuchs, Lecture Notes in Computer Science, 1463, Springer-Verlag, 111--127, 1998.
                                                            • Improving Homeomorphic Embedding for Online Termination.
                                                              In LOPSTR '98, P. Flener, Lecture Notes in Computer Science, 1559, Springer-Verlag, 199--218, 1998.
                                                            • On the Power of Homeomorphic Embedding for Online Termination.
                                                              In Proceedings SAS, Giorgio Levi, Lecture Notes in Computer Science, 1503, Springer-Verlag, 230--245, 1998.
                                                            • Program Specialisation and Abstract Interpretation Reconciled.
                                                              In IJCSLP, J. Jaffar, MIT Press, 220--234, 1998.
                                                            • Michael Leuschel, Danny De Schreye
                                                              Constrained Partial Deduction and the Preservation of Characteristic Trees.
                                                              In New Generation Computing, 16, 3, 283--342, 1998.
                                                              • Michael Leuschel, Danny De Schreye
                                                                Creating Specialised Integrity Checks Through Partial Evaluation of Meta-interpreters.
                                                                In Journal of Logic Programming, 36, 2, 149--193, 1998.
                                                              • Michael Leuschel, Bern Martens, Danny De Schreye
                                                                Controlling Generalisation and Polyvariance in Partial Deduction of Normal Logic Programs.
                                                                In ACM Transactions on Programming Languages and Systems, 20, 1, 208--258, 1998.
                                                                • Michael Leuschel, Bern Martens, Danny De Schreye
                                                                  Some Achievements and Prospects in Partial Deduction.
                                                                  In ACM Computing Surveys, 30, 3es, 1998.
                                                                  • Michael Leuschel, Bern Martens, Konstantinos Sagonas
                                                                    Preserving Termination of Tabled Logic Programs While Unfolding.
                                                                    In LOPSTR '97, N. Fuchs, Lecture Notes in Computer Science, 1463, Springer-Verlag, 189--205, 1998.
                                                                  • Konstantinos Sagonas, Michael Leuschel
                                                                    Extending Partial Deduction to Tabled Execution: Some Results and Open Issues.
                                                                    In ACM Computing Surveys, 30, 3es, 1998.

                                                                    1997

                                                                    • Advanced Techniques for Logic Program Specialisation.
                                                                      In AI Communications, 10, 2, 127--128, 1997.
                                                                      • Specialization of Declarative Programs and its Application (workshop overview).
                                                                        In ILPS, MIT Press, 413--414, 1997.
                                                                        • The Ecce Partial Deduction System.
                                                                          In Proceedings of the ILPS'97 Workshop on Tools and Environments for (Constraint) Logic Programming, German Puebla, Universidad Politécnica de Madrid Tech. Rep. CLIP7/97.1, 1997.
                                                                          • Advanced Techniques for Logic Program Specialisation.
                                                                            PhD Thesis, K.U. Leuven, 1997.

                                                                          1996

                                                                          • Jesper Jørgensen, Michael Leuschel
                                                                            Efficiently Generating Efficient Generating Extensions in Prolog.
                                                                            In Dagstuhl Seminar on Partial Evaluation, O. Danvy and R. Glueck and P. Thiemann, Lecture Notes in Computer Science, 1110, Springer-Verlag, 238--262, 1996.
                                                                          • Jesper Jørgensen, Michael Leuschel, Bern Martens
                                                                            Conjunctive Partial Deduction in Practice.
                                                                            In LOPSTR, J. Gallagher, Lecture Notes in Computer Science, 1207, Springer-Verlag, 59--82, 1996.
                                                                          • Specialised Integrity Checking by Combining Conjunctive Partial Deduction and Abstract Interpretation.
                                                                            In Proc. Logic Databases and the Meaning of Change: Dagstuhl-Seminar-Report 157, J. Bocca and H. Decker and A. Voronkov, IBFI GmbH, Schloss Dagstuhl, 18--19, 1996.
                                                                            • Michael Leuschel, Danny De Schreye
                                                                              Logic Program Specialisation: How To Be More Specific.
                                                                              In Proceedings PLILP'96, H. Kuchen and S. D. Swierstra, Lecture Notes in Computer Science, 1140, Springer-Verlag, 137--151, 1996.
                                                                            • Michael Leuschel, Danny De Schreye
                                                                              Logic Program Specialisation: How To Be More Specific (abstract).
                                                                              In LOPSTR, J. Gallagher, Lecture Notes in Computer Science, 1207, Springer-Verlag, 58, 1996.
                                                                              • Michael Leuschel, Danny De Schreye, D. Andre de Waal
                                                                                A Conceptual Embedding of Folding into Partial Deduction: Towards a Maximal Integration.
                                                                                In JICSLP, M. Maher, MIT Press, 319--332, 1996.
                                                                              • Michael Leuschel, Bern Martens
                                                                                Global Control for Partial Deduction through Characteristic Atoms and Global Trees.
                                                                                In Dagstuhl Seminar on Partial Evaluation, O. Danvy and R. Glueck and P. Thiemann, Lecture Notes in Computer Science, 1110, Springer-Verlag, 263--283, 1996.
                                                                              • Michael Leuschel, Morten Heine Sørensen
                                                                                Redundant Argument Filtering of Logic Programs.
                                                                                In LOPSTR, J. Gallagher, Lecture Notes in Computer Science, 1207, Springer-Verlag, 83--103, 1996.

                                                                                1995

                                                                                • Michael Leuschel, Danny De Schreye
                                                                                  Towards Creating Specialised Integrity Checks Through Partial Evaluation of Meta-Interpreters.
                                                                                  In PEPM, ACM Press, 253--263, 1995.
                                                                                • Michael Leuschel, Danny De Schreye, Bern Martens
                                                                                  Tutorial on Program Specialisation (abstract).
                                                                                  In ILPS, MIT Press, 615--616, 1995.
                                                                                  • Michael Leuschel, Bern Martens
                                                                                    Obtaining Specialised Update Procedures through Partial Deduction of the Ground Representation.
                                                                                    In Proc. Joint Workshop on Deductive Databases and Logic Programming and Abduction in Deductive Databases and Knowledge Based Systems, GMD-Studien Nr. 266, 81--95, 1995.
                                                                                    • Michael Leuschel, Bern Martens
                                                                                      Partial Deduction of the Ground Representation and its Application to Integrity Checking.
                                                                                      In ILPS, MIT Press, 495--509, 1995.

                                                                                      1994

                                                                                      • Partial Evaluation of the "Real Thing".
                                                                                        In LOPSTR, Lecture Notes in Computer Science, 883, Springer-Verlag, 122--137, 1994.
                                                                                        Responsible for the content: