ToC

2024

2023

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.