ProB

ProB is an animator, constraint solver and model checker for the B-Method. It allows fully automatic animation of B specifications, and can be used to systematically check a specification for a wide range of errors. The constraint-solving capabilities of ProB can also be used for model finding, deadlock checking and test-case generation. It allows fully automatic animation of B specifications, and can be used to systematically check a specification for a wide range of errors. The constraint-solving capabilities of ProB can also be used for model finding, deadlock checking and test-case generation.

Publications

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

Preprint Project

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

Preprint Project

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

Preprint Project

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

Project

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

PDF Project

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

Preprint PDF Project

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

PDF Project

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

Preprint PDF Project

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

Preprint PDF Project

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

Preprint PDF Project

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

PDF Project

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

PDF Project

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

Project Poster

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

Preprint PDF Project

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

Preprint PDF Project

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

PDF Project

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

Preprint PDF Project