Publikationen

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.
    PDF
  • 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.
    PDF
  • Proof Assisted Symbolic Model Checking for B and Event-B.
    In Proceedings ABZ 2016, LNCS, 9675, Springer, 2016.
    PDF
  • Interactive Model Repair by Synthesis.
    In Proceedings ABZ 2016, LNCS, 9675, Springer, 2016.
    PDF
  • SMT Solvers for Validation of B and Event-B models.
    In Proceedings iFM 2016, LNCS, 9681, Springer, 2016.
    PDF
  • 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.
    PDF
  • Ivaylo Dobrikov, Michael Leuschel
    Enabling Analysis for Event-B.
    In Proceedings ABZ 2016, LNCS, 9675, Springer, 2016.
    PDF
  • 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).
    In 2016.
    PDF
  • Ivaylo Dobrikov, Daniel Plagge,, Michael Leuschel
    LTL Model Checking under Fairness in ProB.
    In Proceedings SEFM'16, LNCS, 9763, Springer, 2016.
    PDF
  • Meta-Predicates for Rodin.
    In 6th Rodin User and Developer Workshop, 2016.
    PDF
  • The Burden of High-Level Languages: Complicated Symbolic Model Checking.
    In PhD Symposium at iFM'16 on Formal Methods: Algorithms, Tools and Applications, 2016.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • Krings, Sebastian, Leuschel, Michael
    Inferring Physical Units in Formal Models.
    In Software & Systems Modeling, Springer Berlin Heidelberg, 1-23, 2015.
    PDF
  • Translating B to TLA+ for Validation with TLC.
    In 2015.
    PDF
  • Lukas Ladenberger, Michael Leuschel
    Mastering the Visualization of Larger State Spaces with Projection Diagrams.
    In 2015.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • 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.
    In 2014.
    PDF
  • Turning Failure into Proof: Evaluating the ProB Disprover.
    In Proceedings of the 1st International Workshop about Sets and Tools, 2014.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • Integrating ProB into the TLA Toolbox.
    In TLA Workshop, 2014.
    PDF
  • Translating B to TLA + for Validation with TLC.
    In Proceedings ABZ'14, LNCS 8477, 40--55, 2014.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • Parallel Model Checking of B Specifications.
    In Proceedings of the 4th Rodin User and Developer Workshop, TUCS Lecture Notes, TUCS, 2013.
    PDF
  • B constrained.
    In Proceedings of the 4th Rodin User and Developer Workshop, TUCS Lecture Notes, TUCS, 2013.
    PDF
  • Inferring Physical Units in B Models.
    In Proceedings SEFM'2013, LNCS 8137, Springer, 137--151, 2013.
    PDF
  • Michael Jastram
    The Eclipse Requirements Modeling Framework.
    In Managing Requirements Knowledge, Maalej, Walid and Thurimella, Anil, Springer, 2013.
    PDF
  • Stefan Hallerstede
    On Sequentiality and Concurrency,.
    In 2013.
    PDF
  • Stefan Hallerstede, Michael Jastram, Lukas Ladenberger
    A Method and Tool for Tracing Requirements into Specifications.
    In 2013.
    PDF
  • Carl Friedrich Bolz, Lukas Diekmann, Laurence Tratt
    Storage strategies for collections in dynamically typed languages.
    In Proc. OOPSLA, to appear, ACM, 2013.
    PDF
  • 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.
    PDF
  • Translating B to TLA+ for Validation with TLC.
    In 2013.
    PDF

2012

  • Thierry Lecomte, Lilian Burdy, Michael Leuschel
    Formally Checking Large Data Sets in the Railways.
    In CoRR, abs/1210.6815, 2012.
    PDF
  • Translating TLA+ to B for Validation with ProB.
    In Proceedings iFM'2012, LNCS 7321, Springer, 24--38, 2012.
    PDF
  • 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.
    PDF
  • Lukas Ladenberger, Michael Jastram
    Requirements Traceability between Textual Requirements and Formal Models Using ProR.
    In 2012.
    PDF
  • Ingo Weigelt
    Architectures for an Extensible Text Editor for Rodin.
    In 2012.
    PDF
  • Michael Jastram, Andreas Graf
    ReqIF – the new Requirements Standard and its Open Source implementation Eclipse RMF.
    In 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.
    PDF
  • Michael Jastram
    The ProR Approach: Traceability of Requirements and System Descriptions.
    In 2012.
    PDF
  • Christof Ebert, Michael Jastram
    ReqIF: Seamless Requirements Interchange Format between Business Partners.
    In IEEE Software, 82--87, 2012.
    PDF
  • Ardö, Håkan, Bolz, Carl Friedrich, Fijałkowski, Maciej
    Loop-Aware Optimizations in PyPy’s Tracing JIT.
    In DLS, 2012.
    PDF
  • Michael Jastram
    A Systems Engineering Tool Chain Based on Eclipse and Rodin.
    In Forms/Format, 2012.
    PDF

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.
    PDF
  • 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).
    In 2011.
    PDF
  • Michael Jastram, Andreas Graf
    Requirement Traceability in Topcased with the Requirements Interchange Format (RIF/ReqIF).
    In First Topcased Days Toulouse, 2011.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • Stefan Hallerstede, Michael Leuschel
    Finding Deadlocks of Event-B Models by Constraint Solving.
    In B2011 Workshop (short paper), 2011.
    PDF
  • 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.
    PDF
  • Michael Jastram
    ProR - Eine Softwareplattform für Requirements Engineering.
    In Softwaretechnik-Trends, 31, 1, Gesellschaft für Informatik (GI), 2011.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • Michael Jastram, Stefan Hallerstede, Lukas Ladenberger
    Mixing Formal and Informal Model Elements for Tracing Requirements.
    In AVOCS 2011, 2011.
    PDF

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.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • Stefan Hallerstede
    Structured Event-B Models and Proofs.
    In ABZ 2010, Lecture Notes in Computer Science, Springer-Verlag, 2010.
    PDF
  • 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.
    PDF
  • Michael Leuschel, Thierry Massart
    Efficient Approximate Verification of B via Symmetry Markers.
    In Annals of Mathematics and Artificial Intelligence, 59, 1, 81--106, 2010.
    PDF
  • 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.
    PDF
  • David Schneider, Carl Friedrich Bolz, Michael Leuschel
    Jitting Prolog for Fun and Profit.
    In DYLA 2010 - 4th Workshop on Dynamic Languages and Applications, 2010.
    PDF
  • 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.
    PDF
  • Michael Jastram
    ProR, an Open Source Platform for Requirements Engineering based on RIF.
    In SEISCONF, 2010.
    PDF
  • 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.
    In 2010.
    PDF
  • 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.
    PDF

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.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • Daniel Plagge, Michael Leuschel, Ilya Lopatkin, Alex, er Romanovsky
    SAL, Kodkod, and BDDs for Validation of B Models. Lessons and Outlook.
    In Proceedings AFM 2009, 16--22, 2009.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • Stefan Hallerstede
    How to make mistakes.
    In TFM-B 2009, University of Nantes, 93--108, 2009.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • Corinna Spermann, Michael Leuschel
    ProB gets Nauty: Effective Symmetry Reduction for B and Z Models.
    In Proceedings TASE 2008, IEEE, 15--22, 2008.
    PDF
  • 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.
    PDF
  • Declarative Programming for Verification: Lessons and Outlook.
    In Proceedings PPDP'2008, ACM Press, 1--7, 2008.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • Michael Leuschel, Marc Fontaine
    Probing the Depths of CSP-M: A new FDR-compliant Validation Tool.
    In ICFEM 2008, Springer-Verlag, 278--297, 2008.
    PDF
  • A Semantics-Aware Editing Environment for Prolog in Eclipse.
    In Proceedings of the 18th Workshop on Logic-based methods in Programming Environments, WLPE, 2008.
    PDF
  • 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.
    PDF
  • Stefan Hallerstede
    Incremental system modelling in Event-B.
    In FMCO 2008, Lecture Notes in Computer Science, Springer-Verlag, 139--158, 2008.
    PDF
  • 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.
    PDF
  • 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.
    PDF

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.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • Michael Leuschel, Thierry Massart
    Efficient Approximate Verification of B via Symmetry Markers.
    In Proceedings International Symmetry Conference, 71--85, 2007.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • Debugging Event-B Models using the ProB Disprover Plug-in.
    In Proceedings AFADL'07, 2007.
    PDF
  • Carl Friedrich Bolz, Armin Rigo
    How to not write Virtual Machines for Dynamic Languages.
    In Proceeding of Dyla 2007, 2007.
    PDF
  • Michael Leuschel, Daniel Plagge
    Seven at one stroke: LTL model checking for High-level Specifications in B, Z, CSP, and more.
    In 2007.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • Michael Butler, Stefan Hallerstede
    The Rodin Formal Modelling Tool.
    In BCS-FACS Christmas 2007 Meeting, 2007.
    PDF

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.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • Michael Leuschel, Stephen Craig
    A Reconstruction of the Lloyd-Topor Transformation using Partial Evaluation.
    In Pre-Proceedings of LOPSTR'05, Pat Hill, 2005.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • Stephen Craig, Michael Leuschel
    Self-Tuning Resource Aware Specialisation for Prolog.
    In Proceedings PPDP'2005, ACM Press, 23--34, 2005.
    PDF
  • Stefan Hallerstede
    The Event-B Proof Obligation Generator.
    In 2005.
    PDF
  • Stefan Hallerstede, Laurent Voisin
    The Event-B Static Checker.
    In Rodin Deliverable D10, 2005.
    PDF

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.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • ProB: Un outil de modélisation formelle (Invited Talk).
    In JFPLC, Fred Mesnard, Hermes Science Publications, Lavoisier, 13--13, 2004.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • Michael Leuschel, Edd Turner
    Visualising Larger State Spaces in ProB.
    In 2004.
  • Stephane Lo Presti, Michael Butler, Michael Leuschel, Colin Snook, Phillip Turner
    Formal Modelling and Verification of Trust in a Pervasive Application.
    In 2004.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • Michael Leuschel, Stephen Craig, Maurice Bruynooghe, Wim Vanhoof
    Specializing Interpreters using Offline Partial Deduction.
    In 2003.
    PDF
  • 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.
    PDF
  • 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.
    In 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.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • Mauricio Varea, Bashir Al-Hashimi, Michael Leuschel
    Finite and Infinite Model Checking of Dual Transition Petri Net Models.
    In AVoCS, 265--269, 2002.
    PDF
  • 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.
    PDF

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.
    PDF
  • Design and Implementation of the High-Level Specification Language CSP(LP).
    In PADL, Lecture Notes in Computer Science, 1990, Springer, 14--28, 2001.
    PDF
  • 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.
    PDF
  • 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.
    In 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.
    PDF
  • Michael Leuschel, Maurice Bruynooghe
    Control Issues in Partial Deduction: The Ever Ending Story.
    In 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.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • 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.
    In 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.
    PDF
  • 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.
    In 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.
    PDF
  • 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.
    PDF
  • Improving Homeomorphic Embedding for Online Termination.
    In LOPSTR '98, P. Flener, Lecture Notes in Computer Science, 1559, Springer-Verlag, 199--218, 1998.
    PDF
  • 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.
    PDF
  • Program Specialisation and Abstract Interpretation Reconciled.
    In IJCSLP, J. Jaffar, MIT Press, 220--234, 1998.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • 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.
    In 1997.
    PDF
  • Stefan Hallerstede
    Semantische Fundierung von CSP-Z.
    In 1997.
    PDF

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.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • 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.
    PDF
  • 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.
    In 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.
    PDF
  • 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.
Verantwortlich für den Inhalt: E-Mail sendenWE Informatik