Constraint Solving

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 …

Contraint Logic Programming over Infinite Domains with an Application to Proof

We present a CLP(FD)-based constraint solver able to deal with unbounded domains. It is based on constraint propagation, resorting to enumeration if all other methods fail. An important aspect is detecting when enumeration was complete and if this …

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 …

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 tools lack support for annotating variables with (physical) units of measurement. There is thus no obvious way to …

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 …

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 tools lack support for annotating variables with (physical) units of measurement. There is thus no obvious way to …

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 …

B constrained

In a previous work, we applied constraint solving techniques to problems like invariant preservation and deadlock freedom checking. The idea behind constraint based deadlock checking is that we set up a logical formula encoding a state where the …