Generation accounting improves stability of SMT solver proofs
A Deeper Look at Depth: Stable Generation Accounting for Quantifier Reasoning
Logic in Computer Science
Summary
When software tries to check if programs are correct, it often uses special tools called SMT solvers. These solvers can sometimes be unstable—small changes can make them take much longer or fail unexpectedly. The authors studied why this happens and found that the way these tools keep track of certain logic steps (called quantifier instantiations) causes this problem. They created a new way to track these steps that leads to much more stable results without slowing the solver down. Their improvements could help make software verification more reliable.
What this means in practice
- •For software verification engineers: Produce more reliable automated proofs for program correctness by using stable generation accounting in SMT solvers.
- •For formal methods tool developers: Incorporate the new stable accounting method into SMT solvers to reduce proof failures and timeouts during formal verification.
Authors
Can Cebeci, Nikolaj Bjørner, George Candea, Clément Pit-Claudel
Abstract
SMT solvers make automated verification convenient. At the same time, solvers suffer from instability, whereby seemingly inconsequential changes to the input may cause a previously quickly produced proof to fail or time out. This paper addresses a common cause of outcome instability (i.e., unsat/unknown fluctuations) in the context of program verification. We demonstrate that the generation (i.e., depth) accounting used to make quantifier instantiation practical and implemented in multiple state-of-the-art SMT solvers is non-confluent (i.e., prone to divergence), and that this leads to instability. We then address this deficiency and develop a new accounting method that is stable. The new method is justified using a sequence of refinements from an abstract, confluent solver model all the way to our implementation in Z3. Our empirical evaluation demonstrates that our implementation reduces outcome instability by 94% in the unstable core of the Mariposa benchmark without leading to performance regressions.