Z3 | Formal Methods Tools

Quick Links

At a Glance

Developers	Microsoft Research
Domains	Software Verification Hardware Verification Embedded Systems
Formalisms	first-order logic SMT-LIB quantifier logic bit-vectors arrays uninterpreted functions arithmetic
Interactions	CLI Python API Rust Bindings playground
Languages	SMT-LIB Python C++ Java C#
Purposes	Verification Tools Analysis Tools
Systems	Discrete Systems Concurrent Systems
Techniques	Theorem Proving SMT Solving Model Checking

Description

Z3 is a high-performance SMT solver and theorem prover developed by Microsoft Research. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 supports the SMT-LIB standard and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.

Features

SMT Solver: Supports a wide range of theories and quantifiers.
Multi-language APIs: Python, C++, Java, .NET, and more.
Cross-platform: Available on Windows, Linux, and macOS.
Active development: Open source and maintained by Microsoft Research.
Web Playground: Try Z3 online at Rise4Fun.

Publications

Z3: An Efficient SMT Solver (March 2008) by de Moura, Leonardo et. al. | Appears in TACAS | Published by Springer, Berlin, Heidelberg
10.1007/978-3-540-78800-3_24