Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Correctness Witness Validation by Abstract Interpretation

Simmo Saan, Michael Schwarz, Julian Erhard, Helmut Seidl, Sarah Tilscher, Vesal Vojdani

TL;DR

The paper tackles validating correctness witnesses for automated program analyzers using abstract interpretation. It introduces the unassume operator to inject witness invariants into the abstract state, accelerating fixpoint convergence and sometimes increasing precision. The authors implement two forms: propagating unassume for non-relational domains and a dual-narrowing variant for relational domains, and validate them in Goblint with hand-crafted and model-checker witnesses. Experiments show speedups of 7–47% CPU time on multi-threaded benchmarks and that model-checker witnesses can enable verification that the analyzer cannot achieve unaided.

Abstract

Witnesses record automated program analysis results and make them exchangeable. To validate correctness witnesses through abstract interpretation, we introduce a novel abstract operation unassume. This operator incorporates witness invariants into the abstract program state. Given suitable invariants, the unassume operation can accelerate fixpoint convergence and yield more precise results. We demonstrate the feasibility of this approach by augmenting an abstract interpreter with unassume operators and evaluating the impact of incorporating witnesses on performance and precision. Using manually crafted witnesses, we can confirm verification results for multi-threaded programs with a reduction in effort ranging from 7% to 47% in CPU time. More intriguingly, we discover that using witnesses from model checkers can guide our analyzer to verify program properties that it could not verify on its own.

Correctness Witness Validation by Abstract Interpretation

TL;DR

The paper tackles validating correctness witnesses for automated program analyzers using abstract interpretation. It introduces the unassume operator to inject witness invariants into the abstract state, accelerating fixpoint convergence and sometimes increasing precision. The authors implement two forms: propagating unassume for non-relational domains and a dual-narrowing variant for relational domains, and validate them in Goblint with hand-crafted and model-checker witnesses. Experiments show speedups of 7–47% CPU time on multi-threaded benchmarks and that model-checker witnesses can enable verification that the analyzer cannot achieve unaided.

Abstract

Witnesses record automated program analysis results and make them exchangeable. To validate correctness witnesses through abstract interpretation, we introduce a novel abstract operation unassume. This operator incorporates witness invariants into the abstract program state. Given suitable invariants, the unassume operation can accelerate fixpoint convergence and yield more precise results. We demonstrate the feasibility of this approach by augmenting an abstract interpreter with unassume operators and evaluating the impact of incorporating witnesses on performance and precision. Using manually crafted witnesses, we can confirm verification results for multi-threaded programs with a reduction in effort ranging from 7% to 47% in CPU time. More intriguingly, we discover that using witnesses from model checkers can guide our analyzer to verify program properties that it could not verify on its own.
Paper Structure (29 sections, 1 theorem, 29 equations, 4 figures, 2 tables)

This paper contains 29 sections, 1 theorem, 29 equations, 4 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Witnesses
  4. Abstract Interpretation
  5. Initialization-Based Approaches
  6. Total Initial Values.
  7. Partial Initial Values.
  8. Unassuming
  9. Specification
  10. Naïve Definition
  11. Dual-Narrowing
  12. Unassuming Indirectly
  13. Propagating Unassume
  14. Evaluation.
  15. Assume.
  16. ...and 14 more sections

Key Result

theorem 1

Assume a witness $(W, P, \Phi)$ is used to insert unassume statements and $\sigma_W: \mathcal{N} \to \mathbb{D}$ is the result of analyzing the instrumented program. If the sound analyzer confirms $\Phi$ and all invariants of $W: \mathcal{N} \to \mathcal{E}$ abstractly evaluate to true in $\sigma_W$

Figures (4)

  • Figure 0: Syntax of expressions and conditions.
  • Figure 1: Forward evaluation of expressions and conditions.
  • Figure 2: Assume via backward evaluation of expressions and conditions by the propagation algorithm.
  • Figure 3: Unassume via backward evaluation of expressions and conditions by the propagation algorithm (changes from the assume algorithm are $\colorbox{lightyellow}{$\text{highlighted}$}$).

Theorems & Definitions (6)

  • definition 1
  • definition 2
  • theorem 1: Sound witness validation
  • definition 3: Naïve unassume
  • definition 4: Dual-narrowing unassume
  • definition 5: Exploding unassume