Publications

(2019). Prolog Coding Guidelines: Status and Tool Support. In Technical Communications ICLP 2019, EPTCS (to appear).

PDF Project

(2019). Towards Constraint Logic Programming over Strings for Test Data Generation. Accepted for WLP 2019.

Project

(2019). The History and Evolution of B and Event-B. Extended Abstract and Talk at HFM 2019.

PDF Project

(2019). Embedding High-Level Formal Specifications into Applications. In Proceedings FM 2019, Springer LNCS (to appear).

PDF Project

(2019). Automated Backend Selection for ProB Using Deep Learning. In Proceedings NFM 2019, Springer LNCS.

PDF Project Project DOI

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

PDF Project Project

(2018). Measuring Code Coverage of Prolog Programs Using Mutation Testing. In Proceedings WFLP 2018, Springer LNCS.

PDF Project Slides DOI

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

PDF Project Project DOI

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

PDF Project DOI

(2018). From Software Specifications to Constraint Programming. In Proceedings SEFM 2018, Springer LNCS.

PDF Project DOI

(2018). Using a Formal B Model at Runtime in a Demonstration of the ETCS Hybrid Level 3 Concept with Real Trains. In Proceedings ABZ 2018, Springer LNCS.

PDF Project DOI

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

PDF Project DOI

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

PDF DOI

(2017). plspec - A Specification Language for Prolog Data. In Proceedings DECLARE 2017, Springer LNCS.

PDF Project DOI

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

Project DOI

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

PDF Project

(2017). Contraint Logic Programming over Infinite Domains with an Application to Proof. In Proceedings WLP 2016, EPTCS.

PDF Project Project DOI

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

PDF Project

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

PDF Project DOI

(2016). Meta-Predicate for Rodin. In Proceedings Rodin User and Developer Workshop 2016.

PDF Project

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

PDF Project DOI

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

PDF Project Project DOI

(2015). Turning Failure into Proof: The ProB Disprover for B and Event-B. In Proceedings SEFM 2015, Springer LNCS.

PDF Project DOI

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

PDF Project Project DOI

(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.

Project DOI

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

PDF Project

(2014). Who watches the watchers: Validating the ProB Validation Tool. In Proceedings F-IDE 2014, EPTCS.

PDF Project Project DOI

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

PDF Project

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

PDF Project Project DOI

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

Project