Introduction

Z3 is a 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 integrated with a number of program analysis, testing, and verification tools from Microsoft Research. These include: Spec#/Boogie, Pex, Yogi, Vigilante, SLAM, F7, SAGE, VS3, FORMULA, and HAVOC. It can read problems in SMT-LIB and Simplify formats.

Links:

• Introduction

• Documentation

• Download

• Publications and Slides

• Papers With Z3 Applications

• People

• Mailing Lists & Forums

• FAQ (Frequently Asked Questions)

• Z3 Blog

• Awards

• Status

• SMT Links