SMT Solving

Embedding SMT-LIB into B for Interactive Proof and Constraint Solving

Paper presentation.