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]