Jump to content Jump to search

Publications

2024

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.
  • Jannik Dunkelau, Manh Khoi Duong
    Towards Equalised Odds as Fairness Metric in Academic Performance Prediction.
    In 2nd Workshop on Fairness, Accountability, and Transparency in Educational Data, 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.
    • Philipp Körner, Michael Leuschel, João Barbosa, Vtor Santos Costa, Verónica Dahl, Manuel V. Hermenegildo, José F. Morales, Jan Wielemaker, Daniel Diaz, Salvador Abreu
      Fifty Years of Prolog and Beyond.
      In Theory and Practice of Logic Programming, 22, 6, 776--858, 2022.
    • Philipp Körner, Florian Mager
      An embedding of B in Clojure.
      In Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings, MODELS 2022, Montreal, Quebec, Canada, October 23-28, 2022, ACM, 598--606, 2022.
    • Towards Practical Partial Order Reduction for High-Level Formalisms.
      In Verified Software. Theories, Tools and Experiments - 14th International Conference, VSTTE 2022, Trento, Italy, October 17-18, 2022, Revised Selected Papers, Lecture Notes in Computer Science, 13800, Springer, 72--91, 2022.
    • Anne Brecklinghaus, Philipp Körner
      A Jupyter Kernel for Prolog.
      In Proceedings of the 36th Workshop on (Constraint) Logic Programming (WLP 2022), 2022.

    2021

    2020

    2019

    2018

    2017

    • plspec - A Specification Language for Prolog Data.
      In Proceedings Declare 2017, Dietmar Seipel and Michael Hanus and Salvador Abreu, Technical Report, 499, University of Würzburg, 2017.
      • Constraint Modelling and Data Validation Using Formal Specification Languages.
        PhD Thesis, Heinrich-Heine-Universität Düsseldorf, 2017.
      • Janine Golov, Jens Bendisposto
        (Teil)-Invertierung der Programmierausbildung.
        In Inverted Classroom - The next Stage, Lernen und Lehren im 21. Jahrhundert, Sabrina Zeaiter and Jürgen Handke, Tectum, 29--37, 2017.

        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.
          • Meta-Predicates for Rodin.
            In 6th Rodin User and Developer Workshop, 2016.
          • The Burden of High-Level Languages: Complicated Symbolic Model Checking.
            In PhD Symposium at iFM'16 on Formal Methods: Algorithms, Tools and Applications, 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

                • Stefan Hallerstede, Michael Leuschel, Daniel Plagge
                  Validation of Formal Models by Refinement Animation.
                  In Science of Computer Programming, 78, 3, 272--292, 2013.
                • Jens Bendisposto, Joy Clark, Ivaylo Dobrikov, Philipp Körner, Sebastian Krings, Lukas Ladenberger, Michael Leuschel, Daniel Plagge
                  ProB 2.0 Tutorial.
                  In Proceedings of the 4th Rodin User and Developer Workshop, TUCS Lecture Notes, TUCS, 2013.
                • Parallel Model Checking of B Specifications.
                  In Proceedings of the 4th Rodin User and Developer Workshop, TUCS Lecture Notes, TUCS, 2013.
                • B constrained.
                  In Proceedings of the 4th Rodin User and Developer Workshop, TUCS Lecture Notes, TUCS, 2013.
                • Inferring Physical Units in B Models.
                  In Proceedings SEFM'2013, LNCS 8137, Springer, 137--151, 2013.
                • Michael Jastram
                  The Eclipse Requirements Modeling Framework.
                  In Managing Requirements Knowledge, Maalej, Walid and Thurimella, Anil, Springer, 2013.
                • Stefan Hallerstede
                  On Sequentiality and Concurrency,.
                  Unpublished, 2013.
                • Stefan Hallerstede, Michael Jastram, Lukas Ladenberger
                  A Method and Tool for Tracing Requirements into Specifications.
                  Unpublished, 2013.
                • Carl Friedrich Bolz, Lukas Diekmann, Laurence Tratt
                  Storage strategies for collections in dynamically typed languages.
                  In Proc. OOPSLA, to appear, ACM, 2013.
                • Jerome Falampin, Hung Le-Dang, Michael Leuschel, Mikael Mokrani, Daniel Plagge
                  Improving Railway Data Validation with ProB.
                  In Industrial Deployment of System Engineering Methods, Springer, 27--44, 2013.
                • Translating B to TLA+ for Validation with TLC.
                  Technical Report, Institut für Informatik, Heinrich-Heine-Universität Düsseldorf, STUPS/2013/xx, 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.
                • Lukas Ladenberger, Michael Jastram
                  Requirements Traceability between Textual Requirements and Formal Models Using ProR.
                  Unpublished, 2012.
                • Ingo Weigelt
                  Architectures for an Extensible Text Editor for Rodin.
                  Technical Report, University of Düsseldorf, 2012.
                • Michael Jastram, Andreas Graf
                  ReqIF – the new Requirements Standard and its Open Source implementation Eclipse RMF.
                  Technical Report, Commercial Vehicle Technology Symposium, 2012.
                  • Schneider, David, Bolz, Carl Friedrich
                    The Efficient Handling of Guards in the Design of RPython’s Tracing JIT.
                    In VMIL, accepted for publication, 2012.
                  • Michael Jastram
                    The ProR Approach: Traceability of Requirements and System Descriptions.
                    In 2012.
                  • Christof Ebert, Michael Jastram
                    ReqIF: Seamless Requirements Interchange Format between Business Partners.
                    In IEEE Software, 82--87, 2012.
                  • Ardö, Håkan, Bolz, Carl Friedrich, Fijałkowski, Maciej
                    Loop-Aware Optimizations in PyPy’s Tracing JIT.
                    In DLS, 2012.
                  • Michael Jastram
                    A Systems Engineering Tool Chain Based on Eclipse and Rodin.
                    In Forms/Format, 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.
                  • Michael Jastram, Andreas Graf
                    Requirements, Traceability and DSLs in Eclipse with the Requirements Interchange Format (RIF/ReqIF).
                    Technical Report, Dagstuhl-Workshop MBEES 2011: Modellbasierte Entwicklung eingebetteter Systeme, 2011.
                  • Michael Jastram, Andreas Graf
                    Requirement Traceability in Topcased with the Requirements Interchange Format (RIF/ReqIF).
                    In First Topcased Days Toulouse, 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.
                  • Michael Jastram
                    ProR - Eine Softwareplattform für Requirements Engineering.
                    In Softwaretechnik-Trends, 31, 1, Gesellschaft für Informatik (GI), 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.
                  • Michael Jastram, Stefan Hallerstede, Lukas Ladenberger
                    Mixing Formal and Informal Model Elements for Tracing Requirements.
                    In AVOCS 2011, 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.
                  • Stefan Hallerstede
                    Structured Event-B Models and Proofs.
                    In ABZ 2010, Lecture Notes in Computer Science, Springer-Verlag, 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.
                  • Michael Jastram
                    ProR, an Open Source Platform for Requirements Engineering based on RIF.
                    In SEISCONF, 2010.
                  • Proceedings of AVoCS 2010 and Rodin 2010.
                    In Jens Bendisposto and Michael Leuschel and Markus Roggenbach and Stefan Hallerstede and Michael Butler and Laurent Voisin, 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.
                      • Integrated Formal Methods: Proceedings iFM 2009.
                        In Michael Leuschel and Heike Wehrheim, Lecture Notes in Computer Science, 5423, Springer-Verlag, 2009.
                        • Carl Friedrich Bolz, Antonio Cuni, Maciej Fijalkowski, Armin Rigo
                          Tracing the Meta-Level: PyPy's Tracing JIT Compiler.
                          In ICOOOLPS 2009, ACM, 18--25, 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.
                          • Formal Methods and Software Engineering, 11th International Conference on Formal Engineering Methods, ICFEM 2009, Rio de Janeiro, Brazil, December 9-12, 2009. Proceedings.
                            In Karin K. Breitman and Ana Cavalcanti, Lecture Notes in Computer Science, 5885, Springer, 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.
                          • Jean-Raymond Abrial, Michael Butler, Stefan Hallerstede, Thai Son Hoang, Farhad Mehta, Laurent Voisin
                            Rodin: An Open Toolset for Modelling and Reasoning in Event-B.
                            In Software Tools for Technology Transfer, 2009.
                            • Stefan Hallerstede
                              On the Purpose of Event-B Proof Obligations.
                              In Formal Aspects of Computing, Springer-Verlag, 2009.
                              • Stefan Hallerstede, Michael Leuschel
                                How to explain mistakes.
                                In TFM 2009, Lecture Notes in Computer Science, Springer-Verlag, 105--124, 2009.
                              • Stefan Hallerstede
                                How to make mistakes.
                                In TFM-B 2009, University of Nantes, 93--108, 2009.
                              • Stefan Hallerstede
                                Proving Quicksort correct in Event-B.
                                In Refine 2009, ENTCS, 2009.
                                • Stefan Hallerstede
                                  A (Small) Improvement of Event-B?.
                                  In Proceedings of Dagstuhl Seminar on Refinement Based Methods for the Construction of Dependable Systems (09381), 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.
                                  • Carl Friedrich Bolz, Adrian Kuhn, Nicholas Matsakis, Adrian Lienhard, Oscar Nierstrasz, Lukas Renggli, Armin Rigo, Toon Verwaest
                                    Back to the Future in One Week – Implementing a Smalltalk VM in PyPy.
                                    In Self-Sustaining Systems, Lecture Notes in Computer Science, Springer, 123--139, 2008.
                                  • Stefan Hallerstede
                                    Incremental system modelling in Event-B.
                                    In FMCO 2008, Lecture Notes in Computer Science, Springer-Verlag, 139--158, 2008.
                                  • Jean-Raymond Abrial, Michael Butler, Stefan Hallerstede, Laurent Voisin
                                    A roadmap for the Rodin Toolset.
                                    In ABZ 2008, Lecture Notes in Computer Science, Verlag, 347--347, 2008.
                                    • Stefan Hallerstede
                                      On the Purpose of Event-B Proof Obligations.
                                      In ABZ 2008, Lecture Notes in Computer Science, Springer-Verlag, 125--138, 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.
                                        • Carl Friedrich Bolz, Armin Rigo
                                          How to not write Virtual Machines for Dynamic Languages.
                                          In Proceeding of Dyla 2007, 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.
                                          • Jean-Raymond Abrial, Stefan Hallerstede
                                            Refinement, Decomposition, and Instantiation of Discrete Models: Application to Event-B.
                                            In Fundamenta Informaticae, 77, 1-2, 1--28, 2007.
                                          • Stefan Hallerstede, Thai Son Hoang
                                            Qualitative Probabilistic Modelling in Event-B.
                                            In IFM 2007, J. Davies and J. Gibbons, Lecture Notes in Computer Science, Springer-Verlag, 293--312, 2007.
                                          • Stefan Hallerstede
                                            Justifications for the Event-B Modelling Notation.
                                            In B 2007, J. Julliand and O. Kouchnarenko, Lecture Notes in Computer Science, 4591, Springer-Verlag, 293--312, 2007.
                                          • Michael Butler, Stefan Hallerstede
                                            The Rodin Formal Modelling Tool.
                                            In BCS-FACS Christmas 2007 Meeting, 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.
                                            • Jean-Raymond Abrial, Michael Butler, Stefan Hallerstede, Laurent Voisin
                                              An open extensible tool environment for Event-B.
                                              In ICFEM 2006, Lecture Notes in Computer Science, Springer-Verlag, 49--63, 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.
                                                • Stefan Hallerstede
                                                  The Event-B Proof Obligation Generator.
                                                  Technical Report, Information Security, ETH Zürich, 2005.
                                                • Stefan Hallerstede, Laurent Voisin
                                                  The Event-B Static Checker.
                                                  In Rodin Deliverable D10, 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.
                                                    • Dominique Cansell, Stefan Hallerstede, Yann Zimmermann
                                                      Construction sûre de systèmes électroniques.
                                                      In Génie Logiciel, 67, 38--44, 2004.
                                                      • Nikolaos S. Voros, Colin Snook, Stefan Hallerstede, Konstantinos Masselos
                                                        Embedded System Design Using Formal Model Refinement: An Approach Based on the Combined Use of UML and the B Language.
                                                        In Design Automation for Embedded Systems, 9, 2, Springer-Verlag, 67--99, 2004.
                                                        • Stefan Hallerstede, Michael Butler
                                                          Performance analysis of probabilistic action systems.
                                                          In Formal Aspects of Computing, 16, 4, Springer-Verlag, 313--331, 2004.
                                                          • Stefan Hallerstede, Yann Zimmermann
                                                            Circuit Design by Refinement in Event-B.
                                                            In Proceedings of the Forum on Specification and Design Languages (FDL'04), 2004.
                                                            • Nikolaos S. Voros, Colin Snook, Stefan Hallerstede, Thierry Lecomte
                                                              Embedded System Design Using the PUSSEE Method.
                                                              In UML-B Specification for Proven Embedded Systems Design, J. Mermet, Kluwer, 37--52, 2004.
                                                              • Stefan Hallerstede
                                                                BHDL.
                                                                In UML-B Specification for Proven Embedded Systems Design, J. Mermet, Kluwer, 109--120, 2004.
                                                                • Yann Zimmermann, Stefan Hallerstede, Dominique Cansell
                                                                  Formal Modelling of Electronic Circuits Using Event-B, Case Study: SAE J1708 Serial Communication Link.
                                                                  In UML-B Specification for Proven Embedded Systems Design, J. Mermet, Kluwer, 211--226, 2004.
                                                                  • Dominique Cansell, Stefan Hallerstede, Ian Oliver
                                                                    UML-B Specification and Hardware Implementation of a Hamming Coder/Decoder.
                                                                    In UML-B Specification for Proven Embedded Systems Design, J. Mermet, Kluwer, 261--278, 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.
                                                                    • Generative Programming and Component Engineering, Second International Conference, GPCE 2003, Erfurt, Germany, September 22-25, 2003, Proceedings.
                                                                      In Frank Pfenning and Yannis Smaragdakis, Lecture Notes in Computer Science, 2830, Springer, 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.
                                                                      • Proceedings of the 3rd Workshop on Automated Verification of Critical Systems (AVoCS'03).
                                                                        In Michael Leuschel and Stefan Gruner and Stephane Lo Presti, 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.
                                                                        • Proceedings of the 2003 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM'03).
                                                                          In Michael Leuschel, ACM Press, 2003.
                                                                          • Stefan Hallerstede
                                                                            Parallel Hardware Design in B.
                                                                            In ZB 2003, Springer-Verlag, 101--102, 2003.
                                                                            • Stefan Hallerstede
                                                                              Specification and Refinement of Hardware Components in B.
                                                                              In System Specification & Design Languages - Best of FDL '02, Kluwer, 315--325, 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.
                                                                                  • Logic Based Program Synthesis and Transformation, Proceedings of LOPSTR'02, Revised Selected Papers.
                                                                                    In Michael Leuschel, Lecture Notes in Computer Science, 2664, 2002.
                                                                                    • Proceedings of the ACM Sigplan International Workshop on Verification and Computational Logic (VCL'2002).
                                                                                      In Michael Leuschel and Ultes-Nitsche, Ulrich, 2002.
                                                                                      • Stefan Hallerstede, Michael Butler
                                                                                        A Performance-oriented Refinement Assistant.
                                                                                        In RCS '02: International Workshop on Refinement of Critical Systems: Methods, Tools and Experience, 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.
                                                                                          • Proceedings of the ACM Sigplan Workshop on Verification and Computational Logic VCL'2001.
                                                                                            In Michael Leuschel and Andreas Podelski and C.R. Ramakrishnan and Ulrich Ultes-Nitsche, 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.
                                                                                              • Stefan Hallerstede
                                                                                                Performance-Oriented Refinement.
                                                                                                PhD Thesis, Electronics and Computer Science, University of Southampton, 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.
                                                                                                      • Proceedings of the Workshop on Verification and Computational Logic VCL'2000.
                                                                                                        In Michael Leuschel and Andreas Podelski and C.R. Ramakrishnan and Ulrich Ultes-Nitsche, 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.
                                                                                                            • Int. Workshop on Optimization and Implementation of Declarative Programs.
                                                                                                              In Michael Leuschel, 30, 2, 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.
                                                                                                                      • Stefan Hallerstede, Michael Butler
                                                                                                                        Refinement of Dynamic Systems.
                                                                                                                        Technical Report, Electronics and Computer Science, University of Southampton, 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.
                                                                                                                                      • Proceedings of the ILPS'97 Workshop on Specialisation of Declarative Programs and its Application.
                                                                                                                                        In Michael Leuschel, K. U. Leuven, Tech. Rep. CW 255, also as DIKU Report 97/30, University of Copenhagen, 1997.
                                                                                                                                        • Advanced Techniques for Logic Program Specialisation.
                                                                                                                                          PhD Thesis, K.U. Leuven, 1997.
                                                                                                                                        • Stefan Hallerstede
                                                                                                                                          Semantische Fundierung von CSP-Z.
                                                                                                                                          Master Thesis, Carl von Ossietzky Universität Oldenburg, 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.
                                                                                                                                              • Michael Jastram
                                                                                                                                                Inspection and Feature Extraction of Marine Propellers.
                                                                                                                                                Master Thesis, Massachusetts Institute of Technology, 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: WE Informatik : Contact by e-mail