SMT-based Model Checking for Recursive Programs

TL;DR

This paper introduces an SMT-based symbolic model checking algorithm for recursive programs that uses both over- and under-approximations to verify safety properties efficiently, demonstrating significant improvements over existing methods.

Contribution

It presents a modular algorithm that maintains both approximations for recursive procedures, incorporating lazy quantifier elimination and interpolation techniques for improved performance.

Findings

Polynomial decision procedure for Boolean Programs

Efficient instantiation for Linear Arithmetic using lazy QE

Significant empirical improvements on SV-COMP benchmarks

Abstract

We present an SMT-based symbolic model checking algorithm for safety verification of recursive programs. The algorithm is modular and analyzes procedures individually. Unlike other SMT-based approaches, it maintains both "over-" and "under-approximations" of procedure summaries. Under-approximations are used to analyze procedure calls without inlining. Over-approximations are used to block infeasible counterexamples and detect convergence to a proof. We show that for programs and properties over a decidable theory, the algorithm is guaranteed to find a counterexample, if one exists. However, efficiency depends on an oracle for quantifier elimination (QE). For Boolean Programs, the algorithm is a polynomial decision procedure, matching the worst-case bounds of the best BDD-based algorithms. For Linear Arithmetic (integers and rationals), we give an efficient instantiation of the algorithm by applying QE "lazily". We use existing interpolation techniques to over-approximate QE and introduce "Model Based Projection" to under-approximate QE. Empirical evaluation on SV-COMP benchmarks shows that our algorithm improves significantly on the state-of-the-art.