ProB

Sep 26, 2018
Go to Project Site

ProB is an animator, constraint solver and model checker for the B-Method. It allows fully automatic animation of B specifications, and can be used to systematically check a specification for a wide range of errors. The constraint-solving capabilities of ProB can also be used for model finding, deadlock checking and test-case generation. It allows fully automatic animation of B specifications, and can be used to systematically check a specification for a wide range of errors. The constraint-solving capabilities of ProB can also be used for model finding, deadlock checking and test-case generation.

Model Checking Formal Methods Constraint Solving
Sebastian Krings
Sebastian Krings
Software Engineer

My interests include software analysis, formal methods and offensive security.

Publications

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
Validation and Real-Life Demonstration of ETCS Hybrid Level 3 Principles Using a Formal B Model
In this article, we present a concrete realisation of the ETCS Hybrid Level 3 concept, whose practical viability was evaluated in a …
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
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
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
Automated Backend Selection for ProB Using Deep Learning
Employing formal methods for software development usually involves using a multitude of tools such as model checkers and provers. Most …
PDF Cite Project Project DOI
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
From Software Specifications to Constraint Programming
Non-deterministic specifications play a central role in the use of formal methods for software development. Such specifications can be …
PDF Cite 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
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 …
PDF Cite Project DOI
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. …
PDF Cite Project DOI
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 …
Cite Project DOI
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 …
PDF Cite Project
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. It is based on constraint propagation, resorting to …
PDF Cite Project Project DOI
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 …
PDF Cite Project
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 …
PDF Cite Project DOI
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, …
PDF Cite Project Project DOI
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. The high-level nature …
PDF Cite Project DOI
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. As the ProB kernel is now capable of …
PDF Cite Project DOI
Inferring Physical Units in Formal Models
Most state-based formal methods, like B, Event-B or Z, provide support for static typing. However, these methods and the associated …
PDF Cite Project Project DOI
From Animation to Data Validation: The ProB Constraint Solver 10 Years On
Various solvers are linked via reification and Prolog co-routines. The overall challenge of ProB is to solve constraints in full …
Cite Project DOI
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 …
PDF Project
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 …
PDF Cite Project Project DOI
Inferring Physical Units in B Models
Most state-based formal methods, like B, Event-B or Z, provide support for static typing. However, these methods and the associated …
PDF Cite Project Project DOI
Turning Failure into Proof: Evaluating the ProB Disprover
The ProB disprover uses constraint solving to try and find counter examples to proof obligations. As the ProB kernel is now capable of …
PDF Cite Project
B constrained
In a previous work, we applied constraint solving techniques to problems like invariant preservation and deadlock freedom checking. The …
PDF Cite Project

Events

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
Three is a crowd: SAT, SMT and CLP on a chessboard
Declarative encodings of chess problems and how to solve them
Jan 8, 2018 4:30 PM — 5:00 PM Los Angeles, USA
Project