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.
SMT
Writing a Model Checker in 80 Days: Reusable Libraries and Custom Implementation
During a course on model checking we developed BMoth, a full-stack model checker for classical B, featuring both explicit-state and symbolic model checking.
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.
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.
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.
Turning Failure into Proof: Evaluating the ProB Disprover
The ProB disprover uses constraint solving to try and find counter examples to proof obligations.