What is ZB2SMT?
ZB2SMT is a Java package integrated with SMT(Satisfiability Modulo Theories) solvers. The motivation for our work is to provide an automatic verification engine to discharge proof obligations from Z, B or extensions of their, tools. The package takes predicates from both the Z and the B notations and yields a boolean value for them.
ZB2SMT uses an extension of BOL to represent B predicates. On the other hand, the package uses a framework provided by the CZT(Community Z Tool), an ongoing effort that implements tools for standard Z, to represent Z predicates. It also provides methods for get a SMT-file that represents a Z/B predicate. This file can be used as input in most SMT solvers, such as: Z3, CVC3 and veriT.
