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.
ProB
The First Twenty-Five Years of Industrial Use of the B Method
The B-Method has an interesting history, where language and tools have evolved over the years.
Translating Alloy and Extensions to Classical B
In this article, we introduce a denotational translation of the specification language Alloy to classical B.
Embedding SMT-LIB into B for Interactive Proof and Constraint Solving
iFM 2019, Bergen, Norway
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.
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.
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.
The History and Evolution of B and Event-B
The B method for software and systems development together with the specification language B and its successor Event-B offer a rich history.
Repair and Generation of Formal Models Using Synthesis
Writing a formal model is a complicated and time-consuming task.
A Translation from Alloy to B
In this paper, we introduce a translation of the specification language Alloy to classical B.
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.
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 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.
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.
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.
Proof Assisted Symbolic Model Checking for B and Event-B
We have implemented various symbolic model checking algorithms, like BMC, k-Induction and IC3 for B and Event-B.
Inferring Physical Units in Formal Models
Most state-based formal methods, like B, Event-B or Z, provide support for static typing.
From Animation to Data Validation: The ProB Constraint Solver 10 Years On
Various solvers are linked via reification and Prolog co-routines.
Who watches the watchers: Validating the ProB Validation Tool
Over the years, ProB has moved from a tool that complemented proving, to a development environment that is now sometimes used instead of proving for applications, such as exhaustive model checking or data validation.
Inferring Physical Units in B Models
Most state-based formal methods, like B, Event-B or Z, provide support for static typing.