Z3 is a theorem prover developed by Microsoft Research. The core of Z3 is an SMT solver but it has many other features.

## Notes related to Z3 theorem prover

SMT-LIB format, SMT solver, VCC verifier

## Papers related to Z3 theorem prover

- Enhancing symbolic execution with veritesting [avgerinos:icse:2014]
- Boogie: A modular reusable verifier for object-oriented programs [barnett:fmco:2005]
- Z3: An efficient SMT solver [demoura:tacas:2008]
- Developing verified programs with Dafny [leino:icse:2013]
- Dafny: An automatic program verifier for functional correctness [leino:lpair:2010]
- Symbolic execution with SymCC: Don't interpret, compile! [poeplau:usenix:2020]
- Interoperability-guided testing of QUIC implementations using symbolic execution [rath:epiq:2018]