Repair and Generation of Formal Models Using Synthesis
Writing a formal model is a complicated and time-consuming task.
Writing a Model Checker in 80 Days: Reusable Libraries and Custom Implementation
During a course on model checking we developed BMoth, a full-stack model checker for classical B, featuring both explicit-state and symbolic model checking.
From Software Specifications to Constraint Programming
Non-deterministic specifications play a central role in the use of formal methods for software development.
A Translation from Alloy to B
In this paper, we introduce a translation of the specification language Alloy to classical B.
Using a Formal B Model at Runtime in a Demonstration of the ETCS Hybrid Level 3 Concept with Real Trains
In this article, we present a concrete realisation of the ETCS Hybrid Level 3 concept, whose practical viability was evaluated in a field demonstration in 2017.
Three is a crowd: SAT, SMT and CLP on a chessboard
Constraint solving technology for declarative formal models has made considerable progress in recent years, and has many applications such as animation of high-level specifications, test case generation, or symbolic model checking.
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.
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.
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.
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.
Meta-Predicate for Rodin
Event-B provides a concise mathematical language for specifying invariants and guards.
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.
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.
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.
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.
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.