Publications

(2019). Experience Report on An Inquiry-Based Course on Model Checking. Proceedings SEUH, CEUR Workshop Proceedings.

Preprint Project

(2018). Measuring Coverage of Prolog Programs Using Mutation Testing. Accepted for WFLP 2018.

Preprint Project Slides

(2018). Repair and Generation of Formal Models Using Synthesis. Proceedings iFM, Springer LNCS.

Preprint Project

(2018). Writing a Model Checker in 80 Days: Reusable Libraries and Custom Implementation. Proceedings AVoCS 2018, Electronic Communications of the EASST.

Preprint Project

(2018). From Software Specifications to Constraint Programming. Proceedings SEFM, 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 ABZ, Springer LNCS.

Project

(2018). A Translation from Alloy to B. Proceedings ABZ, Springer LNCS.

Preprint Project

(2018). Three is a crowd: SAT, SMT and CLP on a chessboard. Proceedings PADL, Springer LNCS.

Preprint

(2017). plspec - A Specification Language for Prolog Data. Proceedings DECLARE, 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 WLP / WFLP, EPTCS.

Preprint PDF

(2016). The Burden of High-Level Languages: Complicated Symbolic Model Checking. Presented at PhD Symposium at iFM.

PDF Project

(2016). SMT Solvers for Validation of B and Event-B models. Proceedings iFM, Springer LNCS.

Preprint PDF Project

(2016). Meta-Predicates for Rodin. Presented at Rodin Workshop.

Preprint PDF

(2016). Proof Assisted Symbolic Model Checking for B and Event-B. Proceedings ABZ, Springer LNCS.

Preprint PDF Project

(2016). Interactive Model Repair by Synthesis. Proceedings ABZ, Springer LNCS.

Preprint PDF

(2015). Turning Failure into Proof: The ProB Disprover for B and Event-B. Proceedings SEFM, 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.

Project Poster

(2014). Who watches the watchers: Validating the ProB Validation Tool. Proceedings SETS, EPTCS.

Preprint PDF Project

(2013). Turning Failure into Proof: Evaluating the ProB Disprover. Proceedings SETS.

PDF Project

(2013). Inferring Physical Units in B Models. Proceedings SEFM, Springer LNCS.

Preprint PDF Project

(2013). B constrained. Proceedings Rodin Workshop, TUCS Lecture Notes.

Preprint PDF Project