Formal Methods

Towards Infinite-State Symbolic Model Checking for B and Event-B
The idea of verifying the correctness of software has been brought up in the early days of computing, for example by Alan Turing in …
PDF Cite Project
The Burden of High-Level Languages: Complicated Symbolic Model Checking
Symbolic model checking algorithms like IC3 have proven to be an effective technique for hardware model checking. Extensions to …
PDF Cite Project
Turning Failure into Proof: The ProB Disprover for B and Event-B
The ProB disprover uses constraint solving to find counter-examples for B proof obligations. As the ProB kernel is now capable of …
PDF Cite Project DOI
From Animation to Data Validation: The ProB Constraint Solver 10 Years On
Various solvers are linked via reification and Prolog co-routines. The overall challenge of ProB is to solve constraints in full …
Cite Project DOI
Turning Failure into Proof: The ProB Disprover
Initially, the ProB disprover used constraint solving to try and find counterexamples to proof obligations generated from Event-B …
PDF Project
Turning Failure into Proof: Evaluating the ProB Disprover
The ProB disprover uses constraint solving to try and find counter examples to proof obligations. As the ProB kernel is now capable of …
PDF Cite Project
B constrained
In a previous work, we applied constraint solving techniques to problems like invariant preservation and deadlock freedom checking. The …
PDF Cite Project