ProB

Prototyping Games Using Formal Methods

Courses on formal methods are often based on examples and case studies, supposed to show students how to apply formal methods in practice. However, examples often fall into one of two categories: First, many are artificial and thus do not relate to …

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 …

The History and Evolution of B and Event-B

Embedding High-Level Formal Specifications into Applications

The common formal methods workflow consists of formalising a model followed by applying model checking and proof techniques. Once an appropriate level of certainty is reached, code generators are used in order to gain executable code. In this paper, …

Repair and Generation of Formal Models Using Synthesis

Writing a formal model is a complicated and time-consuming task. Usually, one successively refines a model with the help of proof, animation and model checking. In case an error such as an invariant violation is found, the model has to be adapted. …

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. Assumptions regarding type or mode are often made implicitly, without being directly represented in the source code. This …

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 languages. The high-level nature of software models accounts for complicated constraints arising in these symbolic …

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 software model checking have been suggested and implemented and seem promising so far. However, using symbolic model …

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 …

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, deadlocks or refinement errors. Errors are presented as counter-example states and traces and should help fixing the …