The four-page tool paper that introduced Z3, Microsoft Research’s satisfiability modulo theories (SMT) solver. SMT asks whether a first-order formula is satisfiable with respect to background theories such as arithmetic, bit-vectors, arrays and uninterpreted functions. The abstract describes Z3 as freely available and already used in software verification and analysis tools.
Findings
- Not checked in the body: I could only reach the abstract and publisher metadata. The paper won the ETAPS Test of Time Award in 2018.
Limits
- Seedling: abstract only.
- A solver answers the question it is given. If the encoding of a robot’s logic or timing is wrong, Z3 proves things about the wrong system.
- Nonlinear real arithmetic and quantifiers can make queries slow or leave them undecided, which bites when the model includes continuous dynamics.
Relevance
Many verification and analysis tools run on Z3, so any robot verification result built on it is only as good as the model fed to it. See runtime monitoring and robust robotics.
Links
- DOI · code
- Subfield: Safety and verification, Robot learning