ProB

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.

Avatar
Sebastian Krings
Postdoc

My research interests include formal methods, model checking and logic programming.

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

(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). From Software Specifications to Constraint Programming. Proceedings 16th International Conference on Software Engineering and Formal Methods (SEFM 2018), Springer LNCS.

Preprint 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

(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). Interactive Model Repair by Synthesis. Proceedings 5th International ABZ Conference ASM, Alloy, B, TLA, VDM, Z (ABZ 2016), Springer LNCS.

Preprint PDF Project Project

(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

(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). 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). Inferring Physical Units in B Models. Proceedings 11th International Conference on Software Engineering and Formal Methods (SEFM 2013), Springer LNCS.

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). B constrained. Proceedings 4th Rodin User and Developer Workshop 2013, TUCS Lecture Notes.

Preprint PDF Project