Constraint Solving

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 supports data types not available in SMT-LIB and vice versa. In this article we suggest a straightforward translation …

Towards Constraint Logic Programming over Strings for Test Data Generation

Paper presentation.

Towards Constraint Logic Programming over Strings for Test Data Generation

Software is notoriously hard to test. Some of the difficulties stem from the test data available for data-intensive applications such as data warehouses. Existing test data might not be diverse enough to enable desired test cases, while at the same …

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 of them again feature different backends and configuration options. Selecting an appropriate configuration for a …

ProB

Animator, constraint solver and (symbolic) model checker for the B-Method.

Measuring Code Coverage of Prolog Programs Using Mutation Testing

Testing is an important aspect in professional software development, both to avoid and identify bugs as well as to increase maintainability. However, increasing the number of tests beyond a reasonable amount hinders development progress. To decide on …

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 more readable, but hard to execute efficiently due to the usually large search space. Constraint programming offers …

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 grammar, each construct is translated into a semantically equivalent component of the B language. In addition to …

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. In this article we …

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. Floyd in 1967. James C. King extended upon the idea of manual verification by suggesting and working …