Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Z3: Theorem Prover

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.

Please visit the real home page of Z3 for a lot more information!

People
Nikolaj Bjorner
Nikolaj Bjorner

Leonardo de Moura
Leonardo de Moura