ProB

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.

Avatar
Sebastian Krings
Postdoc

My research interests include formal methods, model checking and logic programming.

Publications

The common formal methods workflow consists of formalising a model followed by applying model checking and proof techniques. Once an …

Employing formal methods for software development usually involves using a multitude of tools such as model checkers and provers. Most …

Writing a formal model is a complicated and time-consuming task. Usually, one successively refines a model with the help of proof, …

Non-deterministic specifications play a central role in the use of formal methods for software development. Such specifications can be …

In this paper, we introduce a translation of the specification language Alloy to classical B. Our translation closely follows the Alloy …

We have implemented various symbolic model checking algorithms, such as BMC, k-Induction and IC3 for B, Event-B and other modeling …

In general, even though Prolog is a dynamically typed language, predicates may not be called with arbitrarily typed arguments. …

The idea of verifying the correctness of software has been brought up in the early days of computing, for example by Alan Turing in …

We present a CLP(FD)-based constraint solver able to deal with unbounded domains. It is based on constraint propagation, resorting to …

Symbolic model checking algorithms like IC3 have proven to be an effective technique for hardware model checking. Extensions to …

We present an integration of the constraint solving kernel of the ProB model checker with the SMT solver Z3. We apply the combined …

When using B or Event-B for formal specifications, model checking is often used to detect errors such as invariant violations, …

We have implemented various symbolic model checking algorithms, like BMC, k-Induction and IC3 for B and Event-B. The high-level nature …

The ProB disprover uses constraint solving to find counter-examples for B proof obligations. As the ProB kernel is now capable of …

Most state-based formal methods, like B, Event-B or Z, provide support for static typing. However, these methods and the associated …

Various solvers are linked via reification and Prolog co-routines. The overall challenge of ProB is to solve constraints in full …

Initially, the ProB disprover used constraint solving to try and find counterexamples to proof obligations generated from Event-B …

Over the years, ProB has moved from a tool that complemented proving, to a development environment that is now sometimes used instead …

Most state-based formal methods, like B, Event-B or Z, provide support for static typing. However, these methods and the associated …

The ProB disprover uses constraint solving to try and find counter examples to proof obligations. As the ProB kernel is now capable of …

In a previous work, we applied constraint solving techniques to problems like invariant preservation and deadlock freedom checking. The …

Talks

Declarative encodings of chess problems and how to solve them