SMT

Embedding SMT-LIB into B for Interactive Proof and Constraint Solving

The SMT-LIB language and the B language are both based on predicate logic and share the definition of several operators. However, B supports data types not available in SMT-LIB and vice versa. In this article we suggest a straightforward translation …

BMoth

A prototypical model checker focussing on reusable libraries.

Writing a Model Checker in 80 Days: Reusable Libraries and Custom Implementation

During a course on model checking we developed BMoth, a full-stack model checker for classical B, featuring both explicit-state and symbolic model checking. Given that we only had a single university term to finish the project, a particular focus was …

Three is a crowd: SAT, SMT and CLP on a chessboard

Constraint solving technology for declarative formal models has made considerable progress in recent years, and has many applications such as animation of high-level specifications, test case generation, or symbolic model checking. In this article we …

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 1949 or Robert W. Floyd in 1967. James C. King extended upon the idea of manual verification by suggesting and working …

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 solver to B and Event-B predicates, featuring higher-order datatypes and constructs like set comprehensions. To do so …

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 determining whether a search was exhaustive, one can also use the disprover as a prover. In this paper, we explain how …

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 models. Recently, we made the ProB kernel capable of determining whether a search was exhaustive. Hence, one can now …

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 determining whether a search was exhaustive, one can also use the disprover as a prover. In this paper, we compare …