Universität Düsseldorf: Publications

Publications

2023

Manh Khoi Duong, Jannik Dunkelau, José Andrés Cordova, Stefan Conrad
RAPP: A Responsible Academic Performance Prediction Tool for Decision-Making in Educational Institutes.
In BTW 2023, Gesellschaft für Informatik e.V., 2023.
- PDF
- LINK
Fabian Vu, Michael Leuschel
Validation of Formal Models by Interactive Simulation.
In Proceedings ABZ 2023, LNCS, 14010, Springer, 59--69, 2023.
- The final authenticated version is available online at https://doi.org/10.1007/978-3-031-33163-3_5
Sebastian Stock, Fabian Vu, David Geleßus, Michael Leuschel, Atif Mashkoor, Alexander Egyed
Validation by Abstraction and Refinement.
In Proceedings ABZ 2023, LNCS, 14010, Springer, 160--178, 2023.
- The final authenticated version is available online at https://doi.org/10.1007/978-3-031-33163-3_12
David Geleßus, Sebastian Stock, Fabian Vu, Michael Leuschel, Atif Mashkoor
Modeling and Analysis of a Safety-Critical Interactive System Through Validation Obligations.
In Proceedings ABZ 2023, LNCS, 14010, Springer, 284--302, 2023.
- The final authenticated version is available online at https://doi.org/10.1007/978-3-031-33163-3_22

2022

Fabian Vu, Christopher Happe, Michael Leuschel
Generating Domain-Specific Interactive Validation Documents.
In Proceedings FMICS, LNCS, 13487, Springer, 32--49, 2022.
- The final authenticated version is available online at https://doi.org/10.1007/978-3-031-15008-1_4
Fabian Vu, Dominik Brandt, Michael Leuschel
Model Checking B Models via High-Level Code Generation.
In Proceedings ICFEM, LNCS, 13478, Springer, 334--351, 2022.
- The final authenticated version is available online at https://doi.org/10.1007/978-3-031-17244-1_20
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.
- PDF
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.
- LINK
Joshua Schmidt, Michael Leuschel
SMT solving for the validation of B and Event-B models.
In Software Tools for Technology Transfer (STTT), Springer-Verlag, 2022.

2021

Fabian Vu, Michael Leuschel, Atif Mashkoor
Validation of Formal Models by Timed Probabilistic Simulation.
In Proceedings ABZ, LNCS, 12709, Springer, 81--96, 2021.
- The final authenticated version is available online at https://doi.org/10.1007/978-3-030-77543-8_6
Jens Bendisposto, David Geleßus, Yumiko Jansing, Michael Leuschel, Antonia Pütz, Fabian Vu, Michelle Werth
ProB2-UI: A Java-Based User Interface for ProB.
In Proceedings FMICS, LNCS, 12863, Springer, 193--201, 2021.
- The final authenticated version is available online at https://doi.org/10.1007/978-3-030-85248-1_12
Antonio Cerone, Markus Roggenbach, James Davenport, Casey Denner, Marie Farrell, Magne Haveraaen, Faron Moller, Philipp Körner, Sebastian Krings, Peter Olveczky, Bernd-Holger Schlingloff, Nikolay Shilov, Rustam Zhumagambetov
Rooting Formal Methods within Higher Education Curricula for Computer Science and Software Engineering -- A White Paper.
In CCIS, 1301, Springer, 2021.
- The final authenticated version is available online at https://doi.org/10.1007/978-3-030-71374-4_1
- LINK
Sebastian Krings, Philipp Körner
Prototyping Games Using Formal Methods.
In Proceedings FMFun 2019, CCIS, 1301, Springer, 2021.
- The final authenticated version is available online at https://doi.org/10.1007/978-3-030-71374-4_6
Isabel Wingen, Philipp Körner
Effectiveness of Annotation-Based Static Type Inference.
In Proceedings WFLP 2020, LNCS, 12560, Springer, 2021.
- PDF
Philipp Körner, David Schneider, Michael Leuschel
On the Performance of Bytecode Interpreters in Prolog.
In Proceedings WFLP 2020, LNCS, 12560, Springer, 2021.
- PDF
Joshua Schmidt, Michael Leuschel
Improving SMT Solver Integrations for the Validation of B and Event-B Models.
In Formal Methods for Industrial Critical Systems, Alberto Lluch Lafuente and Anastasia Mavridou, LNCS, 12863, Springer International Publishing, 107--125, 2021.
- The final authenticated version is available online at https://doi.org/10.1007/978-3-030-85248-1_7
Jannik Dunkelau, Leo Baldus
Ranking Model Checking Backends for Automated Selection via Classification and Regression Learning.
In 3rd Workshop on Artificial Intelligence and Formal Verification, CEUR Workshop Proceedings, 2987, 83--89, 2021.
- PDF

2020

Sebastian Krings, Michael Leuschel, Joshua Schmidt, David Schneider, Marc Frappier
Translating Alloy and extensions to classical B.
In Science of Computer Programming, 188, 2020.
Dominik Hansen, Michael Leuschel, Philipp Körner, Sebastian Krings, Thomas Naulin, Nader Nayeri, David Schneider, Frank Skowron
Validation and real-life demonstration of ETCS hybrid level 3 principles using a formal B model.
In International Journal on Software Tools for Technology Transfer, 2020.
- LINK
Sebastian Krings, Philipp Körner, Jannik Dunkelau, Chris Rutenkolk
A Verified Low-Level Implementation of the Adaptive Exterior Light and Speed Control System.
In Proceedings ABZ, LNCS, 12071, Springer, 2020.
- PDF
- The final authenticated version is available online at https://link.springer.com/chapter/10.1007/978-3-030-48077-6_30
Philipp Körner, Michael Leuschel, Jannik Dunkelau
Towards a Shared Specification Repository.
In Proceedings ABZ, LNCS, 12071, Springer, 2020.
- PDF
- The final authenticated version is available online at https://link.springer.com/chapter/10.1007/978-3-030-48077-6_22
Sebastian Krings, Joshua Schmidt, Patrick Skowronek, Jannik Dunkelau, Dierk Ehmke
Towards Constraint Logic Programming over Strings for Test Data Generation.
In Declarative Programming and Knowledge Management, LNCS, 12057, Springer, 139--159, 2020.
Jannik Dunkelau, Joshua Schmidt, Michael Leuschel
Analysing ProB’s Constraint Solving Backends.
In Proceedings ABZ, LNCS, 12071, Springer, 107--123, 2020.
- PDF
- The final authenticated version is available online at https://doi.org/10.1007/978-3-030-48077-6_8
Sophia Reinhardt, Joshua Schmidt, Michael Leuschel, Christiane Schüle, Jörg Schipper
VertiGo - Pilot project for nystagmus detection via webcam.
In Laryngo-Rhino-Otologie, 99, Thieme Verlag, 2020.
- LINK
Isabel Wingen, Philipp Körner
Effectiveness of Annotation-Based Static Type Inference.
In Pre-Proceedings WFLP, 2020.
Philipp Körner, David Schneider, Michael Leuschel
On the Performance of Bytecode Interpreters in Prolog.
In Pre-Proceedings WFLP, 2020.
Michael Butler, Philipp Körner, Sebastian Krings, Thierry Lecomte, Michael Leuschel, Luis-Fernando Mejia, Laurent Voisin
The First Twenty-Five Years of Industrial Use of the B Method.
In Proceedings FMICS, LNCS, 12327, Springer, 2020.
- PDF
Philipp Körner, Jens Bendisposto, Jannik Dunkelau, Sebastian Krings, Michael Leuschel
Integrating formal specifications into applications: the ProB Java API.
In Formal Methods in System Design, Springer, 2020.
- LINK
Sophia Reinhardt, Joshua Schmidt, Michael Leuschel, Christiane Schüle, Jörg Schipper
VertiGo – a pilot project in nystagmus detection via webcam.
In Current Directions in Biomedical Engineering , 6, De Gruyter, 2020.
- LINK

2019

Alexandros Efremidis, Joshua Schmidt, Sebastian Krings, Philipp Körner
Measuring Coverage of Prolog Programs Using Mutation Testing.
In Proceedings WFLP 2018, LNCS, 11285, Springer, 2019.
- PDF
- The final authenticated version is available online at https://doi.org/10.1007/978-3-030-16202-3_3
Sebastian Krings, Philipp Körner, Joshua Schmidt
Experience Report on an Inquiry-Based Course on Model Checking.
In Tagungsband des 16. Workshops "Software Engineering im Unterricht der Hochschulen" 2019, 2358, CEUR, 87--98, 2019.
- PDF
Jannik Dunkelau, Sebastian Krings, Joshua Schmidt
Automated Backend Selection for ProB Using Deep Learning.
In NASA Formal Methods, LNCS, 11460, Springer, 130--147, 2019.
- PDF
- The final authenticated version is available online at https://doi.org/10.1007/978-3-030-20652-9_9
Jannik Dunkelau, Michael Leuschel
Fairness-Aware Machine Learning: An Extensive Overview.
Unpublished, 2019.
- PDF
Isabel Wingen, Philipp Körner
An Optional Static Type System for Prolog.
In Pre-Proceedings LOPSTR, 2019.
- PDF
Philipp Körner, Jens Bendisposto, Jannik Dunkelau, Sebastian Krings, Michael Leuschel
Embedding High-Level Formal Specifications into Applications.
In Proceedings FM, LNCS, 11800, Springer, 2019.
- PDF
- The final authenticated version is available online at https://doi.org/10.1007/978-3-030-30942-8_31
Sebastian Krings, Michael Butler, Philipp Körner, Thierry Lecomte, Michael Leuschel, Laurent Voisin
The History and Evolution of B and Event-B.
In Presentation HFM, 2019.
- PDF
Falco Nogatz, Philipp Körner, Sebastian Krings
Prolog Coding Guidelines: Status and Tool Support.
In Proceedings ICLP (Technical Communications), EPTCS, 306, 2019.
- PDF
- LINK
Sebastian Krings, Joshua Schmidt, Patrick Skowronek, Jannik Dunkelau, Dierk Ehmke
Towards Constraint Logic Programming over Strings for Test Data Generation.
In Pre-Proceedings WLP, 2019.
Fabian Vu, Dominik Hansen, Philipp Körner, Michael Leuschel
A Multi-Target Code Generator for High-Level B.
In Proceedings iFM, LNCS, 11918, Springer, 2019.
- PDF
- The final authenticated version is available online at https://doi.org/10.1007/978-3-030-34968-4_25
Sebastian Krings, Philipp Körner
Prototyping Games Using Formal Methods.
In Pre-Proceedings FMFun, 2019.
- PDF
Sebastian Krings, Philipp Körner, Joshua Schmidt
Inquiry- and Research-based Teaching in a Course on Model Checking.
In Pre-Proceedings FMFun, 2019.
- PDF

2018

Sebastian Krings, Michael Leuschel
Proof Assisted Bounded and Unbounded Symbolic Model Checking of Software and System Models.
In Science of Computer Programming, 158, 41-63, 2018.
Philipp Körner, Sebastian Krings
plspec - A Specification Language for Prolog Data.
In Proceedings Declare 2017, Dietmar Seipel and Michael Hanus and Salvador Abreu, LNAI, 10997, Springer, 2018.
- PDF
- The final authenticated version is available online at https://doi.org/10.1007/978-3-030-00801-7_13
Sebastian Krings, Michael Leuschel, Philipp Körner, Stefan Hallerstede, Miran Hasanagic
Three is a crowd: SAT, SMT and CLP on a chessboard.
In Proceedings PADL 2018, LNCS, 10702, Springer, 2018.
- PDF
- The final authenticated version is available online at https://doi.org/10.1007/978-3-319-73305-0_5
Philipp Körner, Jens Bendisposto
Distributed Model Checking Using ProB.
In Proceedings NFM 2018, LNCS, 10811, Springer, 2018.
- PDF
- The final authenticated version is available online at https://doi.org/10.1007/978-3-319-77935-5_18
Philipp Körner, Jeroen Meijer, Michael Leuschel
State-of-the-Art Model Checking for B and Event-B Using ProB and LTSmin.
In Proceedings iFM 2018, LNCS, 11023, Springer, 2018.
- PDF
- The final authenticated version is available online at https://doi.org/10.1007/978-3-319-98938-9_16
Dominik Hansen, Michael Leuschel, David Schneider, Sebastian Krings, Philipp Körner, Thomas Naulin, Nader Nayeri, Frank Skowron
Using a Formal B Model at Runtime in a Demonstration of the ETCS Hybrid Level 3 Concept with Real Trains.
In Proceedings ABZ 2018, Michael Butler and Alexander Raschke and Thai Son Hoang and Klaus Reichl, LNCS, 10817, Springer, 292--306, 2018.
- PDF
- The final authenticated version is available online at https://doi.org/10.1007/978-3-319-91271-4_20
Sebastian Krings, Joshua Schmidt, Carola Brings, Marc Frappier, Michael Leuschel
A Translation from Alloy to B.
In Proceedings ABZ 2018, LNCS, 10817, Springer, 71--86, 2018.
- PDF
Joshua Schmidt, Sebastian Krings, Michael Leuschel
Repair and Generation of Formal Models Using Synthesis.
In Proceedings iFM 2018, LNCS, 11023, Springer, 2018.
Schneider, David, Leuschel, Michael, Witt, Tobias
Model-based problem solving for university timetable validation and improvement.
In Formal Aspects of Computing, 2018.
- LINK
Alexandros Efremidis, Joshua Schmidt, Sebastian Krings, Philipp Körner
Measuring Coverage of Prolog Programs Using Mutation Testing.
In Pre-Proceedings WFLP, 2018.
- PDF
Philipp Körner, Michael Leuschel
Embedding Formal Specifications as Libraries into Applications.
Technical Report, School of Computing, Newcastle University, 1525, 2018.
- LINK
Jannik Dunkelau
Machine Learning and AI Techniques for Automated Tool Selection for Formal Methods.
In Proceedings of the PhD Symposium at iFM’18 on Formal Methods:Algorithms, Tools and Applications, Research Report, 483, University of Oslo, 2018.
- LINK

2017

Philipp Körner, Sebastian Krings
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.
David Schneider
Constraint Modelling and Data Validation Using Formal Specification Languages.
PhD Thesis, Heinrich-Heine-Universität Düsseldorf, 2017.
- LINK
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

Sebastian Krings, Michael Leuschel
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
- LINK
Sebastian Krings, Michael Leuschel
Proof Assisted Symbolic Model Checking for B and Event-B.
In Proceedings ABZ 2016, LNCS, 9675, Springer, 2016.
- PDF
Joshua Schmidt, Sebastian Krings, Michael Leuschel
Interactive Model Repair by Synthesis.
In Proceedings ABZ 2016, LNCS, 9675, Springer, 2016.
- PDF
Sebastian Krings, Michael Leuschel
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
- The final authenticated version is available online at https://doi.org/10.1007/978-3-319-33693-0_18
Ivaylo Dobrikov, Michael Leuschel
Enabling Analysis for Event-B.
In Proceedings ABZ 2016, LNCS, 9675, Springer, 2016.
- PDF
Dominik Hansen, David Schneider, Michael Leuschel
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.
- PDF
- LINK
Ivaylo Dobrikov, Daniel Plagge,, Michael Leuschel
LTL Model Checking under Fairness in ProB.
In Proceedings SEFM'16, LNCS, 9763, Springer, 2016.
- PDF
Sebastian Krings
Meta-Predicates for Rodin.
In 6th Rodin User and Developer Workshop, 2016.
- PDF
Sebastian Krings
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.
Michael Leuschel
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.
- LINK

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.
- LINK
David Schneider, Michael Leuschel, Tobias Witt
Model-Based Problem Solving for University Timetable Validation and Improvement.
In FM 2015: Formal Methods: 20th International Symposium, Lecture Notes in Computer Science (Book 9109), Springer, 487-495, 2015.
Philipp Körner, David Schneider, Michael Leuschel
Evaluating Interpreter Design in Prolog.
In 18. Kolloquium Programmiersprachen und Grundlagen der Programmierung KPS 2015, Schriftenreihe des Instituts für Computersprachen, Springer, 2015.
- LINK
Sebastian Krings, Jens Bendisposto, Michael Leuschel
From Failure to Proof: The ProB Disprover for B and Event-B.
In Proceedings SEFM'2015, LNCS 9276, Springer, 2015.
- PDF
Sebastian Krings, Michael Leuschel
Inferring Physical Units in Formal Models.
In Software & Systems Modeling, Springer Berlin Heidelberg, 1-23, 2015.
- PDF
Dominik Hansen, Michael Leuschel
Translating B to TLA+ for Validation with TLC.
Technical Report, Institut für Informatik, Heinrich-Heine-Universität Düsseldorf, STUPS/2015/Feb, 2015.
- PDF
- LINK
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.
- PDF
- LINK
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
- LINK
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.
- LINK
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.
- PDF
Sebastian Krings, Jens Bendisposto, Michael Leuschel
Turning Failure into Proof: Evaluating the ProB Disprover.
In Proceedings of the 1st International Workshop about Sets and Tools, 2014.
- 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
Jens Bendisposto, Sebastian Krings, Michael Leuschel
Who watches the watchers: Validating the ProB Validation Tool.
In Proceedings of the 1st Workshop on Formal-IDE, EPTCS, 149, Electronic Proceedings in Theoretical Computer Science, 2014.
- 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
Dominik Hansen, Jens Bendisposto, Michael Leuschel
Integrating ProB into the TLA Toolbox.
In TLA Workshop, 2014.
- PDF
Dominik Hansen, Michael Leuschel
Translating B to TLA + for Validation with TLC.
In Proceedings ABZ'14, LNCS 8477, 40--55, 2014.
- PDF
Michael Leuschel, David Schneider
Towards B as a High-Level Constraint Modelling Language.
In Abstract State Machines, Alloy, B, TLA, VDM, and Z, Ait Ameur, Yamine and Schewe, Klaus-Dieter, Lecture Notes in Computer Science, 8477, Springer Berlin Heidelberg, 101-116, 2014.
- PDF
- LINK
Michael Leuschel
Towards Constraint-Solving over Higher-Order Unbounded Datatypes using Formal Methods Tools.
In VPT 2014, Alexei Lisitsa and Andrei Nemytykh, EPiC Series, 28, EasyChair, 1-1, 2014.
- LINK

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
- LINK
Jens Bendisposto, Philipp Körner, Michael Leuschel
Parallel Model Checking of B Specifications.
In Proceedings of the 4th Rodin User and Developer Workshop, TUCS Lecture Notes, TUCS, 2013.
- PDF
Sebastian Krings, Jens Bendisposto, Ivaylo Dobrikov, Michael Leuschel
B constrained.
In Proceedings of the 4th Rodin User and Developer Workshop, TUCS Lecture Notes, TUCS, 2013.
- PDF
Sebastian Krings, Michael Leuschel
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,.
Unpublished, 2013.
- PDF
Stefan Hallerstede, Michael Jastram, Lukas Ladenberger
A Method and Tool for Tracing Requirements into Specifications.
Unpublished, 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
- LINK
Dominik Hansen, Michael Leuschel
Translating B to TLA+ for Validation with TLC.
Technical Report, Institut für Informatik, Heinrich-Heine-Universität Düsseldorf, STUPS/2013/xx, 2013.
- PDF
- LINK

2012

Thierry Lecomte, Lilian Burdy, Michael Leuschel
Formally Checking Large Data Sets in the Railways.
In CoRR, abs/1210.6815, 2012.
- PDF
Dominik Hansen, Michael Leuschel
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.
Unpublished, 2012.
- PDF
Ingo Weigelt
Architectures for an Extensible Text Editor for Rodin.
Technical Report, University of Düsseldorf, 2012.
- PDF
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.
- 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.
- LINK
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.
- PDF
Michael Jastram, Andreas Graf
Requirement Traceability in Topcased with the Requirements Interchange Format (RIF/ReqIF).
In First Topcased Days Toulouse, 2011.
- PDF
Jens Bendisposto, Michael Leuschel
Automatic Flow Analysis for Event-B.
In Proceedings of Fundamental Approaches to Software Engineering (FASE) 2011, Dimitra Giannakopoulou and Fernando Orejas, Lecture Notes in Computer Science, 6603, Springer, 50--64, 2011.
- 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
- LINK
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
Michael Leuschel, Jens Bendisposto
Directed Model Checking for B: An Evaluation and New Techniques.
In SBMF'2010, Jim Davies and Leila Silva and Adenilso da Silva Simão, Lecture Notes in Computer Science, 6527, Springer, 1--16, 2010.
- 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.
Jens Bendisposto, Michael Leuschel, Markus Borgermans
GEPAVAS Gerichtete und parallele Validierung von abstrakten Spezifikationen - Projektreport.
Technical Report, University of Düsseldorf, 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, Alexander 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.
- LINK
Jens Bendisposto, Michael Leuschel
Proof Assisted Model Checking for B.
In Proceedings of ICFEM 2009, Karin Breitman and Ana Cavalcanti, Lecture Notes in Computer Science, 5885, Springer, 504-520, 2009.
- 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
Lukas Ladenberger, Jens Bendisposto, Michael Leuschel
Visualising Event-B Models with B-Motion Studio.
In Proceedings of FMICS 2009, Marı́a Alpuente and Byron Cook and Christophe Joubert, Lecture Notes in Computer Science, 5825, Springer, 202-204, 2009.
- 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
Jens Bendisposto, Michael Leuschel
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
Michael Leuschel
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
Michael Leuschel
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
Jens Bendisposto, Ian Endrijautzki, Michael Leuschel, David Schneider
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
Jens Bendisposto, Michael Leuschel
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
Jens Bendisposto, Michael Leuschel
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
Olivier Ligot, Jens Bendisposto, Michael Leuschel
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.
Technical Report, Institut für Informatik, Heinrich-Heine-Universität Düsseldorf, STUPS/2007/02, 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.
Michael Leuschel, Jens Bendisposto
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
Michael Leuschel
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.
Technical Report, Information Security, ETH Zürich, 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
Michael Leuschel
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
Michael Leuschel
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.
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.
- 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.
- LINK
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.
Technical Report, ECS, University of Southampton, DSSE-TR-2003-5, 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.
Technical Report, ECS, University of Southampton, DSSE-TR-2002-02, 2002.
Michael Leuschel
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
Michael Leuschel
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.
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.
- PDF
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.
- 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.
Michael Leuschel
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.
Michael Leuschel
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.
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.
- 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.
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.
- 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
Michael Leuschel
Improving Homeomorphic Embedding for Online Termination.
In LOPSTR '98, P. Flener, Lecture Notes in Computer Science, 1559, Springer-Verlag, 199--218, 1998.
- PDF
Michael Leuschel
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
Michael Leuschel
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

Michael Leuschel
Advanced Techniques for Logic Program Specialisation.
In AI Communications, 10, 2, 127--128, 1997.
Michael Leuschel
Specialization of Declarative Programs and its Application (workshop overview).
In ILPS, MIT Press, 413--414, 1997.
Michael Leuschel
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.
Michael Leuschel
Advanced Techniques for Logic Program Specialisation.
PhD Thesis, K.U. Leuven, 1997.
- PDF
Stefan Hallerstede
Semantische Fundierung von CSP-Z.
Master Thesis, Carl von Ossietzky Universität Oldenburg, 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
Michael Leuschel
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.
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.
- 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

Michael Leuschel
Partial Evaluation of the "Real Thing".
In LOPSTR, Lecture Notes in Computer Science, 883, Springer-Verlag, 122--137, 1994.

Responsible for the content:

ToC

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

2003

2002

2001

2000

1999

1998

1997

1996

1995

1994