Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Augmenting Interpolation-Based Model Checking with Auxiliary Invariants (Extended Version)

Dirk Beyer, Po-Chun Chien, Nian-Ze Lee

TL;DR

An augmented interpolation-based verification algorithm that injects external invariants into interpolation-based model checking (McMillan, 2003) and improves the run-time efficiency of the proposed invariant-injection approach.

Abstract

Software model checking is a challenging problem, and generating relevant invariants is a key factor in proving the safety properties of a program. Program invariants can be obtained by various approaches, including lightweight procedures based on data-flow analysis and intensive techniques using Craig interpolation. Although data-flow analysis runs efficiently, it often produces invariants that are too weak to prove the properties. By contrast, interpolation-based approaches build strong invariants from interpolants, but they might not scale well due to expensive interpolation procedures. Invariants can also be injected into model-checking algorithms to assist the analysis. Invariant injection has been studied for many well-known approaches, including k-induction, predicate abstraction, and symbolic execution. We propose an augmented interpolation-based verification algorithm that injects external invariants into interpolation-based model checking (McMillan, 2003), a hardware model-checking algorithm recently adopted for software verification. The auxiliary invariants help prune unreachable states in Craig interpolants and confine the analysis to the reachable parts of a program. We implemented the proposed technique in the verification framework CPAchecker and evaluated it against mature SMT-based methods in CPAchecker as well as other state-of-the-art software verifiers. We found that injecting invariants reduces the number of interpolation queries needed to prove safety properties and improves the run-time efficiency. Consequently, the proposed invariant-injection approach verified difficult tasks that none of its plain version (i.e., without invariants), the invariant generator, or any compared tools could solve.

Augmenting Interpolation-Based Model Checking with Auxiliary Invariants (Extended Version)

TL;DR

An augmented interpolation-based verification algorithm that injects external invariants into interpolation-based model checking (McMillan, 2003) and improves the run-time efficiency of the proposed invariant-injection approach.

Abstract

Software model checking is a challenging problem, and generating relevant invariants is a key factor in proving the safety properties of a program. Program invariants can be obtained by various approaches, including lightweight procedures based on data-flow analysis and intensive techniques using Craig interpolation. Although data-flow analysis runs efficiently, it often produces invariants that are too weak to prove the properties. By contrast, interpolation-based approaches build strong invariants from interpolants, but they might not scale well due to expensive interpolation procedures. Invariants can also be injected into model-checking algorithms to assist the analysis. Invariant injection has been studied for many well-known approaches, including k-induction, predicate abstraction, and symbolic execution. We propose an augmented interpolation-based verification algorithm that injects external invariants into interpolation-based model checking (McMillan, 2003), a hardware model-checking algorithm recently adopted for software verification. The auxiliary invariants help prune unreachable states in Craig interpolants and confine the analysis to the reachable parts of a program. We implemented the proposed technique in the verification framework CPAchecker and evaluated it against mature SMT-based methods in CPAchecker as well as other state-of-the-art software verifiers. We found that injecting invariants reduces the number of interpolation queries needed to prove safety properties and improves the run-time efficiency. Consequently, the proposed invariant-injection approach verified difficult tasks that none of its plain version (i.e., without invariants), the invariant generator, or any compared tools could solve.
Paper Structure (36 sections, 3 theorems, 6 equations, 6 figures, 3 tables, 1 algorithm)

This paper contains 36 sections, 3 theorems, 6 equations, 6 figures, 3 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Our Research Goal
  3. Our Contributions
  4. Augmenting IMC with Auxiliary Invariants
  5. Open-Source Implementation and Extensive Evaluation
  6. Motivating Example
  7. Related Work
  8. Invariant Generation
  9. Invariant-Aided Verification
  10. Background
  11. Model Checking
  12. Describing State-Transition Systems
  13. Verifying Safety Properties
  14. Interpolation-Based Model Checking
  15. Craig Interpolation
  16. ...and 21 more sections

Key Result

theorem thmcountertheorem

Given an unsatisfiable formula $A \land B$, there exists an interpolant $\tau$ of this formula such that (1) $A \Rightarrow \tau$ is valid, (2) $\tau \land B$ is unsatisfiable, and (3) $\tau$ only refers to the common variables of $A$ and $B$.

Figures (6)

  • Figure 1: An example C program to motivate how auxiliary invariants help IMC
  • Figure 2: Comparison of the numbers of program unrollings and interpolation queries
  • Figure 3:
  • Figure 4: Quantile plots comparing the run-time of plain and augmented IMC
  • Figure 5: Comparison of wall-time and interpolation time (TO stands for timeout)
  • ...and 1 more figures

Theorems & Definitions (5)

  • theorem thmcountertheorem
  • theorem thmcountertheorem
  • proof
  • theorem thmcountertheorem
  • proof