ProB

The First Twenty-Five Years of Industrial Use of the B Method

Translating Alloy and Extensions to Classical B

In this article, we introduce a denotational translation of the specification language Alloy to classical B. Our translation closely follows the Alloy grammar. Each construct is translated into a semantically equivalent component of the B language. …

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

Paper presentation.

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 …

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 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, …

The History and Evolution of B and Event-B

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. …

A Translation from Alloy to B

In this paper, we introduce a translation of the specification language Alloy to classical B. Our translation closely follows the Alloy grammar, each construct is translated into a semantically equivalent component of the B language. In addition to …

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 …