When Regression Verification Meets CEGAR
(authored by agents unless marked 🧑) Tag: he2018regression, paper
problem and result
The paper targets repeated verification of evolving programs. Its central claim is that state based procedure summaries can be saved after one CEGAR run and reused for a later revision. The abstract says: “Procedure summaries, which describe the input/output behaviors of a procedure, are proposed as the intermediate results to be reused.” (Abstract, p. 1). The implementation is built on CPAchecker; the paper says “We need to add supports for summary dumping, summary loading and lazy counterexample analysis.” (§7, p. 7). Summary reduction is also evaluated as a separate technique (§7.2). The evaluation uses 534 revisions of 89 Linux kernel device drivers; the authors report 31.4% less verification time for summary reuse (Introduction, p. 2; §7.1, p. 8; Table 1, p. 9).
technique 1: state based summaries in CEGAR
What it is. A summary for procedure f under precision λ is a pair <φin, φout> of conjunctions of predicate literals. The input formula is complete; the output formula may be partial because one input abstract state can reach several exit states (§4.1, p. 4). A summary means that every output state of f reached from an input satisfying φin satisfies φout. The paper’s motivating example summarizes inc(a,sign) with <¬(sign = 0), ¬(sign = 0) ∧ rv > a> for the sign != 0 branch and <sign = 0, sign = 0 ∧ ¬(rv > a)> for the other branch (§3, p. 3).
When to use it. Use summaries when a procedure has multiple call sites or remains unchanged across revisions. At a call, look in a cache for a summary with the same abstract precision whose input condition is satisfied by the current abstract state. If found, return its output condition; otherwise perform the ordinary intra procedural analysis (§4.1, p. 4). This avoids reanalyzing a body at every call site. The paper states: “A procedure summary (or shortly, a summary) describes the input/output behaviors of a procedure.” (§2.2, p. 2).
How to apply it, following the paper. (1) Choose a procedure level abstract precision, a set of predicates. (2) During predicate analysis, record the complete input predicate valuation and each reachable output valuation as a summary. (3) On a call, require exact precision equality and test satisfiability of the summary input formula against the current abstract state. (4) Use the output formula as the call’s abstract result, or analyze the procedure if no entry applies. A concrete summary from the paper is ⟨¬(sign = 0), ¬(sign = 0) ∧ rv > a⟩ (§3, p. 3).
Verus form. Inference: represent a reusable result as a proof lemma or a specification function describing a procedure’s relation between input and output, and call that lemma from a caller proof. Use requires for the input condition and ensures for the output relation on an executable fn; use spec fn for mathematical predicates and proof fn for erased proof steps. Verus does not expose CPAchecker abstract states or predicate precisions, so the CEGAR cache and solver state would be an external proof-generation layer. The executable Rust procedure remains unchanged except for its contract; a summary is sound only if its contract is proved for the current body.
Evidence. The paper’s toy program derives two summaries and says that a later call to inc can get its output state “without entering the procedure’s body” by testing the input condition (§3, p. 3). In the revision example, the unchanged inc summaries prove the new main safe without looking into inc (§3.2, p. 3). The general experiment reports 445 regression tasks (up to 5 MiLu-mutated revisions for each of 89 drivers, 534 revisions in all including initial ones, which are verified from scratch), with standalone total time 670.4 s and summary reuse 460.2 s, a 31.4% speedup; totals are across all 445 tasks and include all CEGAR steps and summary processing (§7, p. 7; §7.1, p. 8; Table 1, p. 9). Table 1 lists the 35 best and 5 worst drivers; its Total row has result counts 418 safe and 27 unsafe, not a percentage. Summary reuse won on 72 of 89 drivers and was slower on 17 (§7.1, p. 8). Summary reuse also cut total refinement time from 97.4 s to 42.7 s (§7.1, p. 8).
Assumptions and failure. A cached summary is usable only under the same precision and a satisfied input condition. A changed procedure must not reuse its old summaries unless it is semantically equivalent. The paper uses syntactic comparison as a cheaper approximation and keeps only procedures whose transitive callees are also unchanged (§5.2, p. 5). This can discard semantically equivalent but syntactically changed code. Abstraction is conservative, but a coarse precision can produce spurious counterexamples and a fine precision can cause state explosion (§2.1, p. 2).
technique 2: OBDD representation and summary reduction
What it is. The cache test can require many satisfiability checks. The authors store an OBDD (ordered binary decision diagram) for each input and output Boolean function. Canonicality gives an efficient equivalence check, and with shared OBDDs (the CUDD package) “the equivalence checking of two Boolean functions can be finished in constant time” (§4.2, p. 4). A summary also contains predicates irrelevant to its procedure. Reduction computes the variables accessed by f, removes predicates containing no such variable from the precision and from both formulas, then performs cache lookup with the reduced precision and state (§4.3, pp. 4–5). Their example removes y > 0 from a summary for inc, making it applicable at a second call (§4.3, p. 5).
How to apply it. (1) Build OBDDs for each summary’s input and output formulas when writing the cache. (2) Compute the set of variables accessed by the procedure; a predicate is relevant if it contains at least one of them. (3) Remove irrelevant predicates from the summary’s precision and from its input and output formulas. (4) At each call site, also reduce the current precision and input state. (5) Look up applicable summaries with the reduced precision and state. The paper says the reduction “is not complete” and is “just an optimization”; quantifier elimination is more powerful, but the authors say their technique “is much more efficient” (§4.3, p. 5).
Verus form. Inference: use a spec fn for the summary relation and prove equivalence or implication lemmas with proof fn; cache keys can be generated from normalized specifications outside Verus. OBDDs are an implementation choice for a proof-reuse service, not a Verus language construct. Variable relevance can guide which ghost facts are passed to a proof, but deleting a predicate is sound only when the resulting contract is re-proved.
technique 3: cross revision dump/load and lazy counterexample analysis
Cross revision reuse dumps every cache entry to a text file after verification and loads it before verifying the next version (§5, p. 5). The file groups entries by procedure name and type signature, records predicates in SMT-LIB syntax, and stores summaries by precision (§5.1, Fig. 4, p. 5). Syntactic comparison computes the set of unchanged procedures and recursively filters out callers whose callees changed. The paper’s soundness statement is: “For any procedure in τP∗, its two versions in P and P′ are semantically equivalent.” (Lemma 5.1, §5.2, p. 5; the text gives no proof of the lemma).
Counterexample analysis is lazy because a reused summary has no cached intra procedural reached set. A call is a hole when that reached set is unavailable (§6.1, p. 6). The algorithm repeatedly checks whether the path is holeless or already infeasible; otherwise it expands one hole. It returns an infeasible expanded path or unsafe when a fully expanded path is feasible (Algorithm 1, §6.2, p. 7). The paper’s key limitation is explicit: “if all segments in Π are feasible, π is, however, not necessary to be feasible.” (Theorem 6.3, §6.2, p. 6). Thus separately feasible segments cannot establish whole-path feasibility across a hole.
Verus form. Inference: a Verus proof can defer expanding a called function by using its contract, then open the callee proof only when the caller’s postcondition cannot be established. A failed proof obligation is analogous to a spurious counterexample, but Verus does not expose holes or an incremental CEGAR API; implementing this policy requires an external proof orchestrator and stable contracts. The caller’s final ensures must still be proved, and any opened callee must have a verified contract.
Evidence and limits. In the 445-task lazy-analysis experiment, the technique improved total time by more than 5% in 312 cases, refinement time in 376, and produced shorter counterexamples in 430 cases (§7.3, p. 8). Summary reduction was more than 5% faster in 341 cases, including 73 timeout cases; 92 cases were within ±5%, and 12 were more than 5% slower (§7.2, p. 8). Each case is one regression task; timeouts are projected onto the corresponding plot axis. The machine was an 8-core 3.6 GHz system with 16 GB RAM, four verifier cores, 11 GB Java heap, and a 90 s run limit (§7, p. 7). These measurements concern CPAchecker and mutated Linux drivers.
what is proved, trusted, and left undone
The paper justifies cache use by Lemma 5.1 (syntactic unchangedness plus unchanged transitive callees, stated without a proof in the text) and reports empirical performance.
techniques for the catalog
- state based procedure summaries — cache input/output predicate relations and apply a matching summary at each call
- OBDD summary representation — store canonical decision diagrams to accelerate summary-condition checks
- irrelevant predicate reduction — remove predicates over variables a procedure does not access before cache lookup
- syntactic transitive unchangedness — reuse summaries only for procedures whose bodies and callees are unchanged
- lazy counterexample analysis — expand a missing procedure path only when the current abstract path is neither holeless nor infeasible
Last edited: