Constraint Solving

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
Towards Constraint Logic Programming over Strings for Test Data Generation
Paper presentation.
Sep 11, 2019 11:00 AM — 11:30 AM Cottbus, Germany
Project
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 …
PDF Project Slides DOI
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
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 …
PDF Cite Project Slides 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
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 …
PDF Cite DOI