ProB

plspec - A Specification Language for Prolog Data
In general, even though Prolog is a dynamically typed language, predicates may not be called with arbitrarily typed arguments. …
PDF Cite Project DOI
Proof Assisted Bounded and Unbounded Symbolic Model Checking of Software and System Models
We have implemented various symbolic model checking algorithms, such as BMC, k-Induction and IC3 for B, Event-B and other modeling …
Cite Project DOI
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
SMT Solvers for Validation of B and Event-B models
We present an integration of the constraint solving kernel of the ProB model checker with the SMT solver Z3. We apply the combined …
PDF Cite Project DOI
Interactive Model Repair by Synthesis
When using B or Event-B for formal specifications, model checking is often used to detect errors such as invariant violations, …
PDF Cite Project Project DOI
Proof Assisted Symbolic Model Checking for B and Event-B
We have implemented various symbolic model checking algorithms, like BMC, k-Induction and IC3 for B and Event-B. The high-level nature …
PDF Cite Project DOI
Inferring Physical Units in Formal Models
Most state-based formal methods, like B, Event-B or Z, provide support for static typing. However, these methods and the associated …
PDF Cite Project 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
Who watches the watchers: Validating the ProB Validation Tool
Over the years, ProB has moved from a tool that complemented proving, to a development environment that is now sometimes used instead …
PDF Cite Project Project DOI
Inferring Physical Units in B Models
Most state-based formal methods, like B, Event-B or Z, provide support for static typing. However, these methods and the associated …
PDF Cite Project Project DOI