PaperlayerView exact revision on arXiv

Source-linked AI summary

SMT-based Model Checking for Recursive Programs

Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki

arXiv:1405.4028v2cs.LO

TL;DR

The paper addresses SMT-based safety verification for recursive programs, where unbounded recursion complicates direct checking. It introduces RecMC, which combines under- and over-approximated procedure summaries, and reports theory-dependent guarantees with significant empirical improvement over the state of the art.

  • Problem

    Safety verification of recursive programs is difficult because unbounded recursion is generally undecidable, motivating procedures that can analyze calls without inlining.

  • Method

    RecMC modularly analyzes procedures using under-approximating reachability facts and over-approximating summary facts, with Model Based Projection for Linear Arithmetic quantifier elimination.

  • Results

    RecMC is guaranteed to find a counterexample when one exists over decidable theories, is polynomial for Boolean Programs, and significantly improves on the state of the art empirically.

  • Takeaways & Limitations

    Combining under- and over-approximations avoids reexploration of parts of the state space and supports recursive-program verification directly on the original program model.

  • Takeaways & Limitations

    Extensions to theories such as uninterpreted functions and arrays remain challenging because they lack quantifier elimination.

Abstract

from arXiv · show

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.

1 Introduction

RecMC addresses safety verification for recursive programs by combining under- and over-approximations of procedure summaries. It provides theory-dependent guarantees, polynomial Boolean-Program complexity, and a Linear Arithmetic instantiation using lazy quantifier elimination and Model Based Projection.

  • Motivation: Safety verification of recursive programs is analyzed over program models whose operations are terms in a first-order theory, but unbounded recursion is generally undecidable.Bounded executions can be analyzed with SMT satisfiability queries over the theory.
  • Motivation: Procedure summaries describe input-output behavior, enabling calls to be analyzed without inlining or analyzing callee bodies.For Boolean Programs, finite state spaces support polynomial summary-based algorithms.
  • RecMC: RecMC maintains over-approximating summary facts to block spurious counterexamples and under-approximating reachability facts to analyze calls without inlining.This combination is presented as the algorithm’s main insight for recursive-program model checking.
  • RecMC: For Boolean Programs, RecMC is worst-case polynomial in the number of states, while for programs over decidable theories it is a co-semidecision procedure.The algorithm is guaranteed to find a counterexample if one exists.
  • Linear Arithmetic: Model Based Projection under-approximates quantifier elimination for Linear Rational and Integer Arithmetic, sometimes avoiding complete elimination.The approach addresses existential quantification that would otherwise enlarge reachability facts; Spacer evaluates the implementation on 799 SV-COMP benchmarks.
  • Contributions: The contributions include an SMT-based recursive-program algorithm, Linear Arithmetic MBP functions, a polynomial Boolean-Program procedure, and empirical evaluation.Summary facts are crucial for richer theories even though they do not improve Boolean-Program worst-case complexity.

2 Overview

RecMC alternates bounded-safety checking with an inductiveness check while maintaining reachability and summary maps indexed by stack depth. BndSafety updates these approximations through callee facts, and the example terminates when the summaries become inductive.

  • Overview: RecMC represents bounded safety with assertion maps ρ and σ, which under- and over-approximate procedure behavior respectively.The maps are partitioned by the call-stack bound.
  • Overview: RecMC alternates between deciding bounded safety and checking whether the resulting proof is inductive independently of the stack bound.It terminates when it finds either a counterexample or a proof.
  • BndSafety: BndSafety first uses callee reachability facts to witness property violations, then uses summary facts to establish satisfaction, and otherwise recursively analyzes a callee at bound b −1.These three steps update the reachability and summary maps without requiring immediate inlining.
  • Example: The example program has three procedures: M calls T and D, T recursively calls itself, and D decrements its argument.The illustrated property is ϕ = m0 ≥ 2m + 4.
  • Example: At stack bound 1, BndSafety jumps over two calls to D using its computed reachability fact, then derives summary facts for T and D.The run updates D first with d = d0 −1, derives t0 ≥ 2t for T, and later derives d ≤ d0 −1 for D.
  • Example: The summaries become inductive, allowing RecMC to terminate and declare the example program SAFE.The body of T satisfies its summary assuming its recursive calls do.

3 Preliminaries

The paper formalizes recursive programs and their bounded and unbounded semantics over first-order theories. It defines summary and reachability facts as over- and under-approximations of bounded procedure behavior.

  • Program representation: A program is a finite list of procedures with a designated main procedure, represented logically by parameters, locals, predicates, and a body formula.Procedure-call predicates occur positively in the body formula, supporting a fixed-point semantics.
  • Assumptions: The presentation assumes no internal procedures, procedure parameters, loops, or global variables, without loss of generality for the stated model.Procedures cannot be passed as parameters.
  • Semantics: A procedure’s semantics characterizes its terminating executions and has a least fixed-point characterization.Bounded semantics restricts executions by a call-stack-depth bound and is defined inductively on that bound.
  • Safety properties: A safety property requires every terminating execution of a procedure to satisfy a formula in every model of the underlying theory.The program property is defined through its main procedure.
  • Approximation facts: A summary fact over-approximates bounded procedure semantics, whereas a reachability fact under-approximates it.These facts respectively contain all bounded executions or describe only behaviors guaranteed to be reachable.

4 Model Checking Recursive Programs

RecMC checks recursive-program safety modularly by maintaining reachability and summary facts for individual procedures. It is sound, finds counterexamples under decidable-theory assumptions, and is polynomial for Boolean Programs.

  • Algorithm: RecMC maintains reachability and summary assertion maps to under- and over-approximate bounded procedure semantics.It iteratively analyzes procedures individually rather than requiring whole-program inlining.
  • BndSafety: BndSafety answers bounded queries using summary facts, reachability facts, interpolation, and newly generated procedure queries.Negative queries infer over-approximating summaries, while positive queries infer under-approximating reachability facts.
  • Counterexample handling: Potential counterexample paths are partitioned around a procedure call, using an over-approximated prefix and an under-approximated suffix to create a callee query.The resulting query checks whether the suspected path is feasible without inlining the callee.
  • Correctness: RecMC and BndSafety are sound, and BndSafety terminates given an oracle for the theory.Consequently, RecMC is guaranteed to find a counterexample when one exists.
  • Boolean Programs: For Boolean Programs, RecMC terminates after O(N^2 · 2^2k) rule applications, where N is the number of procedures and k is the maximum procedure-state size.The complexity is quadratic in the number of procedures because RecMC uses iterative deepening.

5 Model Based Projection

The paper introduces Model Based Projection to lazily under-approximate existential quantifier elimination in RecMC. For LRA, its projection is model-selected, quantifier-free, and linear in formula size.

  • Motivation: Linear Arithmetic instantiation replaces expensive eager quantifier elimination with lazy, quantifier-free under-approximations.Without elimination, existential variables accumulate and formula size can grow exponentially with call-stack depth.
  • Definition: A Model Based Projection maps models of a quantifier-free matrix to a finite set of quantifier-free formulas covering those models.Each projected formula is satisfied by its associated model and under-approximates the existential formula.
  • LRA projection: LRAProj selects a covering disjunct from a model according to satisfied equality and lower-bound literals, breaking ties syntactically.The construction is based on the Loos-Weispfenning quantifier-elimination method.
  • Properties: Theorem 4 establishes that LRAProj is a Model Based Projection, and its computation is linear in the size of the formula.An analogous MBP for LIA is based on Cooper’s method.
  • Integration: Using MBP in Reach and Query preserves soundness and termination while inferring only the necessary under-approximations.The modified procedure is sound and terminating assuming an oracle and an MBP for the theory.

6 Implementation and Experiments

RecMC is implemented in Spacer and evaluated against Z3's GPDR on Boolean and SV-COMP benchmarks. Spacer performs significantly better on most SV-COMP programs and handles an exponentially growing call-tree example better than Z3.

  • Implementation: Spacer implements RecMC using Z3 for SMT-solving and interpolation, with UFO converting C programs into Z3's Horn-SMT format.The implementation supports propositional logic, linear arithmetic, and bit-vectors via bit-blasting.
  • Benchmarks: The evaluation covers 2,908 Boolean Programs from SLAM and 799 SVCOMP 2014 C programs, plus two more modular variants of the SVCOMP set.Spacer was compared with Z3's GPDR under 30-minute time and 16GB memory limits.
  • Boolean Program Benchmarks: Spacer handles increasing complexity significantly better than Z3 on a Boolean Program whose call-tree size grows exponentially with the number of procedures.This comparison appears in Fig. 9(a), alongside the Boolean benchmark evaluation.
  • SVCOMP 2014 Benchmarks: Spacer is significantly better on most programs in the Svcomp-1, Svcomp-2, and Svcomp-3 scatter plots.Diamonds denote time-outs and stars denote memory-outs in the reported plots.

7 Related Work

Related work frames RecMC against summary-based interprocedural analysis and recent SMT-based recursive-program verifiers. Its distinguishing feature is combining over- and under-approximations of procedure semantics, unlike the closest alternatives described.

  • Summary-Based Analysis: Interprocedural analysis commonly represents each procedure's input-output behavior with summaries, allowing calls to be analyzed without inlining the callee body.For finite Boolean Programs, finite state spaces support polynomial algorithms because summaries can only be updated finitely many times.
  • Approximation Strategies: The related-work discussion emphasizes that prior approaches did not use under-approximations of procedure semantics in the way RecMC does.This distinction is stated directly in the comparison with existing approaches.
  • SMT-Based Verification: Recent SMT-based algorithms use SMT solving for counterexamples and interpolation to over-approximate summaries, but may completely unroll the call graph in the worst case.Corral instead relies on user input and heuristics for summaries.
  • GPDR: GPDR is the closest related algorithm, but unlike RecMC it does not maintain reachability facts and therefore has no Reach rule.GPDR modifies Query to use a satisfying model rather than RecMC's path when creating a query.
  • Approximation Strategies: Earlier combinations of over- and under-approximations under-approximate summaries using must transitions, whereas RecMC uses reachability facts with a different meaning.The paper explicitly distinguishes its reachability facts from the must-transition notion in prior work.

8 Conclusion

The paper concludes that RecMC combines over- and under-approximations to verify recursive programs, with guarantees over decidable theories and an efficient Linear Arithmetic instantiation. Spacer provides empirical evidence of improvement, while extending beyond supported theories remains future work.

  • Conclusion: RecMC is an SMT-based algorithm for safety model checking of recursive programs that combines under- and over-approximations of procedure semantics.The combination is intended to avoid reexploring parts of the state space.
  • Conclusion: For programs and properties over decidable theories, RecMC is guaranteed to find a counterexample if one exists and is polynomial for Boolean Programs.The conclusion identifies this as the first SMT-based algorithm claimed to have both properties.
  • Conclusion: Model-Based Projection provides an efficient Linear Arithmetic instantiation by under-approximating expensive quantifier elimination.The conclusion places this instantiation within the broader RecMC approach.
  • Conclusion: RecMC has been implemented in Spacer, with empirical evidence that it significantly improves on the state of the art.The implementation and empirical result are stated together in the conclusion.
  • Future Work: Extending RecMC to theories such as uninterpreted functions and arrays remains future work because of the lack of quantifier elimination.Combining RecMC with proof-based abstraction is another proposed direction.

C Termination of BndSafety (Proof of Theorem 2)

The termination proof for BndSafety bounds reachability facts and queries, establishes progress and eventual query answering, and concludes termination given an oracle for the background theory.

  • Termination Theorem: Given an oracle for the background theory, BndSafety terminates.This is stated as Theorem 2 after the termination lemmas are introduced.
  • Complexity Parameters: The termination analysis measures complexity using N procedures, p maximum paths per procedure, c maximum calls per path, and call-stack bound n.These parameters are used throughout the update and query bounds.
  • Finite Reach Facts: Reachability facts for a procedure predicate and stack bound are updated only O(N^b · p^(b+1)) times.The bound follows because facts are inferred per path and existing reachability facts prevent duplicate inferences.
  • Finite Queries: Queries are applicable only O(c · N^b · p^(b+1)) times for a procedure, formula, and stack bound.The bound counts path divisions and updates to lower-bound reachability environments.
  • Progress: As long as the query set is nonempty, one of Sum, Reach, or Query is applicable, ensuring progress.Choosing a query with the smallest bound satisfies Query's second side-condition.
  • Eventual Answer: Every query is eventually answered by Sum or Reach in O(b · c^b · (Np)^(O(b^2))) rule applications.Finite query creation and guaranteed rule applicability together establish eventual answering.

D Complexity of RecMC for Boolean Programs (Proof of Theorem 3)

For Boolean Programs, RecMC terminates with a polynomial bound in the number of procedures and states, specifically O(N^2 · 2^2k).

  • RecMC terminates for Boolean Programs in O(N^2 · 2^2k) applications of its rules.This is the stated complexity bound of Theorem 3.
  • With call-stack bound n, BndSafety has complexity O(N · 2^k · n).The bound follows from O(2^k) possible parameter valuations across N procedures and n bound values.
  • The total number of summary facts per procedure is bounded by O(2^k), yielding O(N · 2^k) RecMC iterations.Monotonicity in the bound b supplies the iteration bound.

E BndSafety with MBP (Proof of Theorem 5)

Adding Model Based Projection to BndSafety preserves soundness and termination, while increasing complexity bounds by a factor tied to the MBP image size.

  • BndSafety with an oracle and an MBP remains sound and terminating under the modified rules.This is the statement of Theorem 5.
  • MBP preserves soundness because Sum is unaffected and Reach infers strengthened reachability facts.The modified side conditions preserve the supporting lemmas.
  • If an MBP has image size d, the finiteness arguments for reachability facts and queries acquire an extra factor of d.The remaining finiteness proofs are unchanged, so the complexity bounds are scaled up.
  • Theorem 2 therefore remains valid with a scaled-up complexity bound, and Theorem 5 is unaffected by under-approximations.The result combines preserved finiteness and the unchanged theorem about under-approximations.

F LRAProj λ is an MBP (Proof of Lemma 4)

LRAProj λ is proved to be a Model Based Projection by finite-image virtual substitution, with cases based on equality terms, lower bounds, and −∞.

  • LRAProj λ is a Model Based Projection.This is the section's central theorem.
  • The projection has a finite image because it selects among finitely many disjuncts in the Loos-Weispfenning decomposition.The proof then checks that every model of λ satisfies its selected quantifier-free projection.
  • Virtual substitution evaluates x-containing literals at equality terms e, lower-bound terms ℓ + ǫ, or −∞.The corresponding substitutions map equalities and inequalities to quantifier-free formulas.
  • For each model M, LRAProj λ selects the disjunct indexed by a term whose substituted formula is satisfied by M.The proof establishes this by considering the cases for t and each literal containing x.
  • The analogous LIA construction, LIAProj λ, is based on Cooper’s quantifier-elimination method and is also a Model-Based Projection.Its construction handles divisibility literals through a finite disjunction over residue cases.
Loading 1405.4028v2…