ProB

Integrating Formal Specifications into Applications - The ProB Java API
The common formal methods workflow consists of formalising a model followed by applying model checking and proof techniques. Once an …
PDF Project
The First Twenty-Five Years of Industrial Use of the B Method
PDF Project
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 …
Project DOI
Embedding SMT-LIB into B for Interactive Proof and Constraint Solving
Paper presentation.
Dec 6, 2019 11:30 AM — 12:00 PM Bergen, Norway
Project
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 …
PDF Project Slides DOI
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 …
PDF Project Project Slides
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 …
PDF Cite Project DOI
The History and Evolution of B and Event-B
PDF Project
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, …
PDF Cite Project Project DOI
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 …
PDF Cite Project DOI