Home • Docs • Download • Mail • FAQ • Awards • Status • MSR

Z3 An Efficient SMT Solver

Introduction

Z3 is a new high-performance theorem prover being developed at Microsoft Research. Z3 supports linear real and integer arithmetic, fixed-size bit-vectors, extensional arrays, uninterpreted functions, and quantifiers. Z3 is still under development, but it has already been integrated with Spec#/Boogie, and HAVOC. We are currently integrating Z3 with Pex, SAGE, Yogi, Vigilante, and SLAM. It can read problems in SMT-LIB and Simplify formats.

Links:

Last modified Thu Apr 17 10:57:25 2008