Publications

(2019). Automated Backend Selection for ProB Using Deep Learning. Proceedings 11th Annual NASA Formal Methods Symposium (NFM 2019), Springer LNCS (to appear).

Preprint Project Project

(2019). Experience Report on An Inquiry-Based Course on Model Checking. Proceedings 16. Workshop Software Engineering im Unterricht der Hochschulen (SEUH 2019), CEUR Workshop Proceedings (to appear).

Preprint Project

(2018). Measuring Coverage of Prolog Programs Using Mutation Testing. Proceedings 26th International Workshop on Functional and Logic Programming (WFLP 2018), Springer LNCS.

Preprint PDF Project Slides

(2018). Repair and Generation of Formal Models Using Synthesis. Proceedings 14th International Conference on integrated Formal Methods (iFM 2018), Springer LNCS.

Preprint Project Project

(2018). Writing a Model Checker in 80 Days: Reusable Libraries and Custom Implementation. Proceedings 18th International Workshop on Automated Verification of Critical Systems (AVoCS 2018), Electronic Communications of the EASST.

Preprint Project

(2018). From Software Specifications to Constraint Programming. Proceedings 16th International Conference on Software Engineering and Formal Methods (SEFM 2018), Springer LNCS.

Preprint Project

(2018). Using a Formal B Model at Runtime in a Demonstration of the ETCS Hybrid Level 3 Concept with Real Trains. Proceedings 6th International ABZ Conference ASM, Alloy, B, TLA, VDM, Z (ABZ 2018), Springer LNCS.

Project

(2018). A Translation from Alloy to B. Proceedings 6th International ABZ Conference ASM, Alloy, B, TLA, VDM, Z (ABZ 2018), Springer LNCS.

Preprint Project

(2018). Three is a crowd: SAT, SMT and CLP on a chessboard. Proceedings 20th International Symposium on Practical Aspects of Declarative Languages (PADL 2018), Springer LNCS.

Preprint

(2017). plspec - A Specification Language for Prolog Data. Proceedings Conference on Declarative Programming (DECLARE 2017), Springer LNCS.

Preprint PDF Project

(2017). Proof Assisted Bounded and Unbounded Symbolic Model Checking of Software and System Models. Science of Computer Programming, Elsevier.

PDF Project

(2017). Towards Infinite-State Symbolic Model Checking for B and Event-B. Dissertation submitted to the Heinrich-Heine-University.

Preprint PDF Project

(2017). Contraint Logic Programming over Infinite Domains with an Application to Proof. Proceedings 30th Workshop on (Constraint) Logic Programming (WLP 2016), EPTCS.

Preprint PDF

(2016). The Burden of High-Level Languages: Complicated Symbolic Model Checking. Presented at PhD Symposium at 12th International Conference on integrated Formal Methods (iFM 2016).

PDF Project

(2016). SMT Solvers for Validation of B and Event-B models. Proceedings 12th International Conference on integrated Formal Methods (iFM 2016), Springer LNCS.

Preprint PDF Project

(2016). Meta-Predicates for Rodin. Proceedings of the 6th Rodin User and Developer Workshop 2016.

Preprint PDF Slides

(2016). Proof Assisted Symbolic Model Checking for B and Event-B. Proceedings 5th International ABZ Conference ASM, Alloy, B, TLA, VDM, Z (ABZ 2016), Springer LNCS.

Preprint PDF Project

(2016). Interactive Model Repair by Synthesis. Proceedings 5th International ABZ Conference ASM, Alloy, B, TLA, VDM, Z (ABZ 2016), Springer LNCS.

Preprint PDF Project Project

(2015). Turning Failure into Proof: The ProB Disprover for B and Event-B. Proceedings 13th International Conference on Software Engineering and Formal Methods (SEFM 2015), Springer LNCS.

Preprint PDF Project

(2015). Inferring Physical Units in Formal Models. Software and Systems Modeling, Springer.

PDF Project

(2014). From Animation to Data Validation: The ProB Constraint Solver 10 Years On. In Formal Methods Applied to Complex Systems: Implementation of the B Method.

PDF Project

(2014). Turning Failure into Proof: The ProB Disprover. Poster presented at SAT / SMT Summer School 2014.

Project Poster

(2014). Who watches the watchers: Validating the ProB Validation Tool. Proceedings 1st Workshop on Formal Integrated Development Environment (F-IDE 2014), EPTCS.

Preprint PDF Project

(2013). Turning Failure into Proof: Evaluating the ProB Disprover. Proceedings 1st International Workshop about Sets and Tools (SETS 2014).

PDF Project

(2013). Inferring Physical Units in B Models. Proceedings 11th International Conference on Software Engineering and Formal Methods (SEFM 2013), Springer LNCS.

Preprint PDF Project

(2013). B constrained. Proceedings 4th Rodin User and Developer Workshop 2013, TUCS Lecture Notes.

Preprint PDF Project