Translating Alloy and Extensions to Classical B
In this article, we introduce a denotational translation of the specification language Alloy to classical B.
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.
Towards Constraint Logic Programming over Strings for Test Data Generation
DECLARE 2019, Cottbus, Germany
Towards Constraint Logic Programming over Strings for Test Data Generation
Software is notoriously hard to test.
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.
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.
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.
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.
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.
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.
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.
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.
Inferring Physical Units in B Models
Most state-based formal methods, like B, Event-B or Z, provide support for static typing.
Turning Failure into Proof: Evaluating the ProB Disprover
The ProB disprover uses constraint solving to try and find counter examples to proof obligations.
B constrained
In a previous work, we applied constraint solving techniques to problems like invariant preservation and deadlock freedom checking.