STUPS Group


News

ADVANCE will hold a public Industry Day in Düsseldorf (University House) on Thursday 23rd October 2014 aimed at industrial participants with an interest in engineering methods for software-intensive systems, especially safety-critical systems.

Prof. Egon Börger visited our group during May 2014 as part of an award of the Alexander von Humboldt Foundation.

Teaching

Übersicht über alle vom Lehrstuhl angebotenen Veranstaltungen und langfristige Planung.

Übersicht über freie Themen für Bachelor-, Master- und Projektarbeiten.

Summer 2016

Winter 2015/2016

Latest Publications

2016
Optimising the ProB Model Checker for B using partial order reduction [PDF] [Bibtex]
Formal Aspects of Computing, 28(2): 179-323, 2016.
Meta-Predicates for Rodin [PDF] [Bibtex]
In 6th Rodin User and Developer Workshop, 2016.
The Burden of High-Level Languages: Complicated Symbolic Model Checking [PDF] [Bibtex]
In PhD Symposium at iFM'16 on Formal Methods: Algorithms, Tools and Applications, 2016.
Enabling Analysis for Event-B [PDF] [Bibtex]
In Proceedings ABZ 2016, volume 9675 of LNCS, Springer, 2016.
Interactive Model Repair by Synthesis [PDF] [Bibtex]
In Proceedings ABZ 2016, volume 9675 of LNCS, Springer, 2016.
Proof Assisted Symbolic Model Checking for B and Event-B [PDF] [Bibtex]
In Proceedings ABZ 2016, volume 9675 of LNCS, Springer, 2016.
Using B and ProB for Data Validation Projects [Bibtex]
In Proceedings ABZ 2016, volume 9675 of LNCS, Springer-Verlag, 2016.
BMotionWeb: A Tool for Rapid Creation of Formal Prototypes [Bibtex]
In Proceedings SEFM'16, volume 9763 of LNCS, Springer, 2016.
LTL Model Checking under Fairness in ProB [PDF] [Bibtex]
In Proceedings SEFM'16, volume 9763 of LNCS, Springer, 2016.
SMT Solvers for Validation of B and Event-B models [PDF] [Bibtex]
In Proceedings iFM 2016, volume 9681 of LNCS, Springer, 2016.
Jens Bendisposto, Philipp Koerner, Michael Leuschel, Jeroen Meijer, Jaco van de Pol, Helen Treharne, Jorden Whitefield
Symbolic Reachability Analysis of B through ProB and LTSmin [PDF] [Bibtex]
In Proceedings iFM 2016, volume 9681 of LNCS, Springer, 2016.
Constraint Logic Programming over Infinite Domains with an Application to Proof [Bibtex]
In Proceedings of the 30th Workshop on (Constraint) Logic Programming, 2016.
Enabling Analysis for Event-B (Technical Report) [PDF] [Bibtex]
Technical Report, No. STUPS/2016/xx, Institut für Informatik, University of Düsseldorf, 2016.


2015
Inferring Physical Units in Formal Models [PDF] [Bibtex]
Software & Systems Modeling: 1-23, 2015.
Validation of the ABZ landing gear system using ProB [Bibtex]
International Journal on Software Tools for Technology Transfer: 1-17, 2015.
Model-Based Problem Solving for University Timetable Validation and Improvement [Bibtex]
In FM 2015: Formal Methods: 20th International Symposium, Lecture Notes in Computer Science (Book 9109), Springer, 2015.
Mastering the Visualization of Larger State Spaces with Projection Diagrams [Bibtex]
In Proceedings ICFEM'2015, LNCS 9407, Springer-Verlag, 2015.
From Failure to Proof: The ProB Disprover for B and Event-B [PDF] [Bibtex]
In Proceedings SEFM'2015, LNCS 9276, Springer, 2015.
Mastering the Visualization of Larger State Spaces with Projection Diagrams [PDF] [Bibtex]
Technical Report, No. STUPS/2015/May, Institut für Informatik, Heinrich-Heine-Universität Düsseldorf, 2015.
Translating B to TLA+ for Validation with TLC [PDF] [Bibtex]
Technical Report, No. STUPS/2015/Feb, Institut für Informatik, Heinrich-Heine-Universität Düsseldorf, 2015.
Evaluating Interpreter Design in Prolog [Bibtex]
Technical Report, No. 2015-IX-1, institution, 2015.


Have a look at the publications page for publications in 2014 and before.