33 lines
1.8 KiB
Markdown
33 lines
1.8 KiB
Markdown
+++
|
|
date = 2024-02-02T04:14:54-08:00
|
|
draft = false
|
|
title = 'Z3'
|
|
purposes = ['Verification Tools', 'Analysis Tools']
|
|
techniques = ['Theorem Proving', 'SMT Solving', 'Model Checking']
|
|
domains = ['Software Verification', 'Hardware Verification', 'Embedded Systems']
|
|
languages = ['SMT-LIB', 'Python', 'C++', 'Java', 'C#']
|
|
systems = ['Discrete Systems', 'Concurrent Systems']
|
|
interactions = ['CLI', 'Python API', 'Rust Bindings', 'playground']
|
|
formalisms = ['first-order logic', 'SMT-LIB', 'quantifier logic', 'bit-vectors', 'arrays', 'uninterpreted functions', 'arithmetic']
|
|
developers = ['Microsoft Research']
|
|
licenses = ['MIT']
|
|
links = [
|
|
{ title = "Homepage", url = "https://github.com/Z3Prover/z3" },
|
|
{ title = "Source Code", url = "https://github.com/Z3Prover/z3" },
|
|
{ title = "Discussions", url = "https://github.com/Z3Prover/z3/discussions" },
|
|
{ title = "Documentation", url = "https://z3prover.github.io/api/html/" },
|
|
{ title = "Playground", url = "https://rise4fun.com/z3" }
|
|
]
|
|
publications = ['deMoura2008']
|
|
+++
|
|
|
|
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](https://rise4fun.com/z3).
|