Z3: An efficient SMT solver

Leonardo de Moura, Nikolaj Bjørner
[doi] [Google Scholar] [DBLP] [Citeseer]

International conference on Tools and Algorithms for the Construction and Analysis of Systems
Springer
Pages 337-340
2008
Topic(s): tools verification
Note(s): SMT solver, Z3 solver

Z3 theorem prover

  • Verifying Rust programs with SMACK [baranowski:atva:2018]
  • Specification and verification: The Spec# experience [barnett:cacm:2011]
  • SecChisel: Language and tool for practical and scalable security verification of security-aware hardware architectures [deng:hasp:2019]
  • Dafny: An automatic program verifier for functional correctness [leino:lpair:2010]
  • Scaling symbolic evaluation for automated verification of systems code with Serval [nelson:sosp:2019]
  • A hardware design language for timing-sensitive information flow security [zhang:asplos:2015]