Tunable Automation in Automated Program Verification

TL;DR

This paper introduces a tunable mechanism for controlling quantifier instantiation in SMT-based verification tools, balancing automation and performance, demonstrated through implementation in Verus for Rust codebases.

Contribution

It presents a novel fine-grained control mechanism for quantifier availability in automated verification, allowing customization at various levels to optimize performance and automation.

Findings

Selective quantifier management improves verification efficiency.

Automation-performance tradeoff is evident in empirical results.

Flexible control enhances usability of verification tools.

Abstract

Automated verification tools based on SMT solvers have made significant progress in verifying complex software systems. However, these tools face a fundamental tension between automation and performance when dealing with quantifier instantiation -- the primary source of incompleteness and verification slowdown in SMT-based verifiers. Tools choose between aggressive quantifier instantiation that provides more automation but longer verification times, or conservative instantiation that responds quickly but may require more manual proof hints. We present a mechanism that enables fine-grained control over the availability of quantified facts in verification contexts, allowing developers to selectively tune the level of automation. Our approach lets library authors provide different pre-defined automation levels while giving end-users the ability to further customize quantifier availability at the module, function, or proof context level. We implement our techniques in Verus, a Rust-based verification tool, and evaluate them on multiple openly available codebases. Our empirical analysis demonstrates the automation-performance tradeoff and that selective quantifier management enables developers to select the appropriate level of automation in different contexts.