Intern talk: Understanding and Mitigating Solver Instability in Verification Tools

Опубликовано 27 сентября 2016, 18:29

Abstract: Program verification tools such as Dafny and F* rely on Z3, an SMT-based automated theorem prover, to dispatch verification conditions. Z3's powerful automation relieves programmers of the burden of writing tedious manual proofs. However, since many of the problems Z3 is asked to solve are undecidable in general, Z3 depends on various complex heuristics. This means that minor, seemingly insignificant changes can have large effects on proof time, and can even cause Z3 to fail to produce proofs where it previously succeeded. In this work, we identify various sources of instability and quantify their impacts. We also present preliminary results on a technique borrowed from the domain of large-theory mathematical theorem-proving to mitigate instability and improve performance.