11institutetext: LMU Munich, Munich, Germany

# Augmenting Interpolation-Based Model Checking with Auxiliary Invariants

(Extended Version)††thanks: A conference version [1] of this manuscript is
published at SPIN 2024.

Dirk Beyer Po-Chun Chien Nian-Ze Lee

###### 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.

###### Keywords:

Software model checking Program invariants Invariant injection Craig
interpolation Data-flow analysis SMT SAT

##  1 Introduction

Assuring that programs execute correctly with respect to their specifications
is fundamental for deploying them in our daily lives. In the software
industry, testing [2] is the most popular methodology to validate the quality
of programs. However, software testing can only spot the presence of bugs in
programs but not guarantee their absence. To prove the correctness of programs
with mathematical rigorousness, automatic software model checking [3] has been
extensively studied. One of the greatest challenges to formally verify a
program is to deduce suitable _program invariants_ that can be used to prove
the program’s safety properties. A program invariant is a logical formula over
some program variables that must hold at a certain program location for all
feasible program paths.

There are numerous approaches to invariant generation, with different
performance characteristics and strengths of produced invariants. Data-flow
analysis [4, 5, 6, 7, 8, 9, 10] is a category of methods that sacrifice path
sensitivity for scalability. To reduce the size of the abstract reachability
graph, data-flow analysis merges abstract program states arising from
different execution paths when the control flow meets. Since merging abstract
states usually loses information, the resulting invariants might not be strong
enough to prove the safety properties. In contrast to data-flow analysis,
techniques [11, 12, 13, 14, 15, 16] based on Craig interpolation [17]
iteratively derive interpolants111An interpolant $\tau$ for an implication
$A\Rightarrow B$ is a formula that uses only the common variables of formulas
$A$ and $B$ such that $A\Rightarrow\tau$ and $\tau\Rightarrow B$ are valid. to
construct strong invariants. Although these approaches are capable of
generating useful invariants, they might take too many refinement iterations
and fail to converge.

To leverage the information carried by invariants, researchers also use
invariant generators as an auxiliary component to aid various model-checking
techniques. Algorithms that have been augmented by _invariant injection_
include bounded model checking (BMC) [18, 19, 20], k-induction [21, 22, 23,
24, 25], predicate abstraction [26, 27], symbolic execution [28], and IC3/PDR
[29]. The idea is to confine the scope of a verification algorithm to the
reachable state space of a program, as safety properties often do not hold in
the unreachable parts [22].

###  1.1 Our Research Goal

Despite the extensive study of injecting invariants to various software-
verification methods, the possibilities of leveraging auxiliary invariants to
assist _interpolation-based model checking_ [11], a hardware model-checking
algorithm published by McMillan in 2003 and adopted to software recently [30],
have not been explored yet. Although this algorithm was invented two decades
ago, it still remains state-of-the-art for safety verification. In this paper,
our goal is to find out _whether invariant injection can enhance McMillan’s
interpolation-based model-checking algorithm from 2003 for software
verification_. In particular, we aim to reduce the number of interpolation
queries required to prove the safety property of a program, since
interpolation is usually the most time-consuming step in interpolation-based
algorithms. To avoid confusion between McMillan’s algorithm from 2003 [11] and
other interpolation-based verification approaches, we refer to McMillan’s
approach from 2003 as IMC from now on. IMC has been combined with expensive
SAT-based invariant generators for hardware model checking [31, 32], but its
characteristics when assisted by lightweight invariant generators [33] based
on data-flow analysis remain unknown for software verification.

To motivate how auxiliary invariants could assist IMC, we briefly introduce
the algorithm first. IMC extends BMC via constructing inductive invariants by
Craig interpolants [17] arising from unsatisfiable BMC queries. Whenever a BMC
query starting from initial states is unsatisfiable, IMC derives an
interpolant from the query and replaces the initial states in the query with
the interpolant. If the new query is unsatisfiable again, another interpolant
can be obtained. The process is repeated until either (1) the newest
interpolant is contained in the union of initial states and previous
interpolants, or (2) the query starting from the newest interpolant becomes
satisfiable. In case (1), an inductive invariant (i.e., a fixed point) is
found and the property is proven. In case (2), the satisfied query might be a
spurious counterexample, so IMC will continue to unfold the program.

Interpolants tend to abstract away irrelevant information and may intersect
with the unreachable state space. Therefore, conjoining them with auxiliary
invariants prunes away some unreachable states. In the IMC algorithm outlined
above, if the newest interpolant is strengthened by an auxiliary invariant, it
is more likely to be contained in the union of initial states and previous
interpolants, and the query starting from a strengthened interpolant is less
likely to be satisfiable. In other words, a fixed point might be found with
fewer interpolation queries in case (1), and a spurious alarm plus extra
program unrollings could be avoided in case (2). An example will be shown in
Sect. 1.3 to illustrate these benefits.

###  1.2 Our Contributions

####  1.2.1 Augmenting IMC with Auxiliary Invariants

We devise two methods to augment IMC with auxiliary invariants. The first
method confines the containment check between the newest interpolant and the
union of initial states and previous interpolants with auxiliary invariants.
The strengthened check is more likely to succeed, so a fixed point can be
found with fewer unrollings and interpolation calls. The second method
conjoins derived interpolants with auxiliary invariants. The BMC query
starting from a strengthened interpolant is more likely to be unsatisfiable,
and more interpolants can be derived to form a fixed point before IMC further
unrolls the program. We rigorously prove the correctness of the proposed
techniques. The proposed augmenting approaches are novel because they are the
first invariant-injection techniques for IMC applied to program analysis.
Moreover, the theoretical results in this paper are applicable to IMC for
hardware verification even though we focus on software verification.

####  1.2.2 Open-Source Implementation and Extensive Evaluation

We implemented the proposed approaches in the open-source framework CPAchecker
[34] and conducted an extensive evaluation on more than $1\,600$ difficult
verification tasks of C programs from the 2022 Intl. Competition on Software
Verification [35]. In our experiments, the plain IMC algorithm (i.e., without
invariant injection), three other mature SMT-based algorithms in CPAchecker,
and two other software verifiers were used as references to evaluate our
implementation. Our experimental results show that invariant injection (1)
effectively reduces the numbers of program unrollings and interpolation
queries needed by plain IMC to prove safety properties, (2) reduces the wall-
time usage, (3) proves 16 tasks that neither plain IMC nor the data-flow
analyzer used to generate invariants could solve, and (4) outperformed other
well-established software verifiers. These observations are significant
because they enhance the knowledge about the effect of auxiliary invariants on
IMC. Our open-source implementation of the proposed approaches also helps
other researchers to understand the details of the algorithms better and
provides a solid baseline for future studies.

###  1.3 Motivating Example

⬇ 1extern int nondet(); 2int main(void) { 3 unsigned int x = 0; 4 unsigned int
i = 0; 5 while (nondet()) { 6 x += 2; 7 if (i == 3) x++; 8 i++; 9 if (i == 2)
i = 0; 10 } 11 if (x % 2) { 12 ERROR: return 1; 13 } 14 return 0; 15}

Figure 1: An example C program to motivate how auxiliary invariants help IMC

We use the example C program in Fig. 1 to explain why invariant injection can
reduce the numbers of program unrollings and interpolation queries for IMC. In
the program, variables x and i are both initialized to $0$. The loop will be
executed nondeterministically many times depending on the values returned by
function nondet(). The values of x and i are modified in each loop iteration:
x will be incremented by $2$; if i equals $3$, x will be further incremented
by $1$. Variable i will be incremented by $1$ and reset to $0$ if its value
equals $2$ after being incremented. An error occurs if x is odd when the
control flow exits the loop.

IMC first checks if the error location line 12 is reachable by skipping the
loop. As the conjunction of the initial states $x=0\land i=0$ and the guard to
the error location $x\%2$ is unsatisfiable, namely, line 12 is unreachable if
the loop is skipped, IMC will try to build an inductive invariant at the loop
head line 5 to prove that all paths entering the loop cannot reach the error
location. IMC unrolls the program and builds a BMC query222 The query is
$(x=0\land i=0)\land(i=3\Rightarrow x^{\prime}=x+3)\land(i\neq 3\Rightarrow
x^{\prime}=x+2)\land(i+1=2\Rightarrow i^{\prime}=0)\land(i+1\neq 2\Rightarrow
i^{\prime}=i+1)\land(x^{\prime}\%2\neq 0)$, where the prime symbols indicate
variables after a loop iteration, and the returned values of function nondet()
are omitted for simplicity.  starting from the initial location line 3, going
through the loop once (i.e., visiting line 5 twice), and ending at the error
location line 12. This BMC query is unsatisfiable, so an interpolant at the
loop head line 5 can be derived to overapproximate the program states
reachable after one loop iteration. Assume the interpolant is $x\%2=0$
(instantiated with variables of the initial states). IMC will replace the
initial states $x=0\land i=0$ in the BMC query by $x\%2=0$ and pose another
query to derive the next interpolant. Unfortunately, the new query is
satisfiable, indicating that there exists a feasible path from line 5 to the
error location, which assumes x to be even at the beginning of the path and
goes through the loop body once. Indeed, a solution to the new query is
$(x,i)=(0,3)$, which leads to $x=3$ after exiting the loop. To decide whether
this solution is a spurious counterexample or not, IMC has to further unroll
the program and fails to converge to a fixed point under the current
unrolling. The reason behind this situation is that the interpolant $x\%2=0$
contains unreachable program states allowing the infeasible assignment $i=3$.
In fact, the safety property of the program is fulfilled as variable $i$ never
grows beyond $2$, and the problematic statement x++; at line 7 is unreachable.

By contrast, it is easy for data-flow analysis, e.g., one based on the
abstract domain of intervals [33], to identify that $0\leq i\leq 1$ is an
invariant at line 5 of the program. If this invariant is injected to
strengthen the interpolant $x\%2=0$, IMC reaches a fixed point $0\leq i\leq
1\land x\%2=0$ immediately, without further unrolling the program. This
reasoning is confirmed by our implementation in CPAchecker, which injects
auxiliary invariants produced by a continuously-refining interval analysis
[33] into the plain IMC algorithm [30]. The table below summarizes the first
interpolants obtained at line 5 and the numbers of unrollings and
interpolation queries needed to prove the program in Fig. 1 for the plain and
augmented IMC implementations in CPAchecker.

Algorithm | First interpolant at line 5 | Fixed point | #Unrolling | #Itp-queries
---|---|---|---|---
Plain IMC [30] | $x\%2=0$ | No | 3 | 7
Augmented IMC | $0\leq i\leq 1\land x\%2=0$ | Yes | 1 | 2

##  2 Related Work

Our paper is primarily related to invariant generation and verification
approaches aided by auxiliary invariants.

###  2.1 Invariant Generation

Various approaches exist for invariant generation, ranging from lightweight
ones based on data-flow analysis to computationally expensive ones based on
SAT/SMT solving, predicate abstraction, or Craig interpolation.

Data-flow analysis has been extensively studied [5, 6, 7, 8, 9, 10]. Classic
approaches usually consider program variables over an abstract domain
structured as a semi-lattice. A standard fixed-point procedure is used to
iteratively explore a program, and abstract states reached by different
program traces are merged. When the iteration finishes, the abstract states at
each program location contain corresponding program invariants. Common choices
of abstract domains include a value domain [36, 37] or an interval domain
[38].

Interpolation-based approaches construct invariants by either predicates
collected from interpolants [12] or interpolants themselves [11, 13, 14, 15].
Although they are able to build strong invariants, the expensive interpolation
queries might hinder their scalability. Iterative SAT solving is used to prove
the inductiveness of candidate invariants extracted from simulation data [31].
Invariant generation can also be guided by the safety property [39, 40] or the
syntax of the program [41].

###  2.2 Invariant-Aided Verification

Injecting invariants to enhance model-checking algorithms is a popular
technique. There are techniques to restrict the state space in BMC queries by
high-level design information [19] or data mining [20]. It is well known that
the induction hypothesis of k-induction is often too weak on its own and has
to be strengthened by auxiliary invariants from static analysis [21, 23] or
property-directed reachability [25, 42]. Alternatively, k-induction can be
used to prove candidate invariants instantiated from a template, and the
confirmed invariants can be used in an induction proof [43]. Recently, an
interval-based analysis that produces continuously-refined invariants was
successfully applied to boost the performance of k-induction [22]. Transition
relations can be strengthened by invariants from the octagon abstract domain
to reduce the number of refinement loops in predicate abstraction [27]. Loop
invariants can be used as annotations in symbolic execution [28]. Predicate
abstraction is also employed to improve candidate invariants formed by Craig
interpolants to reduce the number of refinements [44]. IMC is also combined
with inductive invariants to avoid spurious counterexamples in hardware model
checking [32]. Different from continuously-refined invariants commonly used in
software verification, this approach computes a single invariant by SAT
solving and uses it repeatedly throughout the entire verification process.
Spacer [45], the backend engine of the verification framework SeaHorn [29],
uses invariants produced by the abstract-interpretation tool Ikos [46] to
speed up the analysis.

##  3 Background

In this section, we provide necessary background knowledge for the rest of the
paper. All used logical formulas are quantifier-free and belong to the first-
order theory of equality with uninterpreted functions, arrays, bit-vectors,
and floats. We consider the satisfiability and validity of a logical formula
with respect to this theory. A first-order predicate over system states is
interpreted interchangeably

###  3.1 Model Checking

First, we recap the problem formulation of model checking. To simplify the
presentation in Sect. 4, we describe model checking with the notation of
state-transition systems and view a program as a state-transition system. The
implementation of the proposed methods, discussed in Sect. 5, represents a
program as a control-flow automaton and verifies C programs.

####  3.1.1 Describing State-Transition Systems

A state-transition system $M$ is characterized by two predicates $I(s)$ and
$T(s,s^{\prime})$ over all possible states of the system: $I(s)$ evaluates to
true if state $s$ is an initial state of $M$; $T(s,s^{\prime})$ evaluates to
true if $M$ can transit from state $s$ to state $s^{\prime}$. A state-
transition system is denoted by $M=(I(s),T(s,s^{\prime}))$ in the following. A
primed variable is used for a state after transition. We write $R(s)$ to
represent the set of all reachable states of $M$.

####  3.1.2 Verifying Safety Properties

Model checking concerns if a state-transition system fulfills a safety
property. A safety property can be described as a predicate $P(s)$ that
evaluates to true if state $s$ satisfies the property. Given a state-
transition system $M=(I(s),T(s,s^{\prime}))$ and a safety property $P(s)$, $M$
fulfills $P(s)$ if $R(s)\Rightarrow P(s)$ is valid, namely, the property is
satisfied by all reachable states of $M$. Model-checking algorithms receive
$M=(I(s),T(s,s^{\prime}))$ and $P(s)$ as input and aim at proving or
disproving $R(s)\Rightarrow P(s)$.

We discuss two criteria widely used by model-checking algorithms to establish
$R(s)\Rightarrow P(s)$. First, some approaches construct an _inductive_ set
$F(s)$ that implies $P(s)$. That is, $F(s)$ must conform to the constraint
below:

$\displaystyle(I(s)\Rightarrow F(s))\land(F(s)\land T(s,s^{\prime})\Rightarrow
F(s^{\prime}))\land(F(s)\Rightarrow P(s)).$

Since $R(s)$ is the smallest inductive set of $M$, we have $R(s)\Rightarrow
F(s)$. The implication $R(s)\Rightarrow P(s)$ follows from $R(s)\Rightarrow
F(s)$ and $F(s)\Rightarrow P(s)$. Interpolation-based approaches such as IMC
[11] and interpolation-sequence-based model checking [14] fall into this
category because they try to build an inductive state set from Craig
interpolants.

The second criterion takes advantage of _invariants_. An invariant $Inv(s)$ of
$M$ is a predicate that holds for all reachable states of $M$, namely,
$R(s)\Rightarrow Inv(s)$ is valid. Given an invariant $Inv(s)$ of $M$, some
methods produce a set $G(s)$ that is _relatively inductive_ to $Inv(s)$ and
implies $P(s)$. In other words, $G(s)$ must fulfill:

$\displaystyle(I(s)\Rightarrow G(s))\land(Inv(s)\land G(s)\land
T(s,s^{\prime})\Rightarrow G(s^{\prime}))\land(G(s)\Rightarrow P(s)).$ (1)

Because $Inv(s)$ holds for every reachable state and $G(s)$ is relatively
inductive to $Inv(s)$, we have $R(s)\Rightarrow G(s)$. The implication
$R(s)\Rightarrow P(s)$ is thus concluded from $R(s)\Rightarrow G(s)$ and
$G(s)\Rightarrow P(s)$. IC3/PDR [40] is a prominent example based on this
criterion. It chooses $G(s)$ to be the safety property $P(s)$ and generates
clauses to form an invariant to which $P(s)$ is relatively inductive. As will
be seen in Sect. 4, instead of producing invariants internally during model
checking, we leverage external invariant generators and augment IMC to compute
a relatively inductive set to the auxiliary invariants.

###  3.2 Interpolation-Based Model Checking

IMC is an algorithm proposed by McMillan in 2003 [11]. Originally designed for
hardware verification, it has been adopted to analyze software recently [30].
IMC extends BMC by constructing inductive invariants (i.e., fixed points) from
_Craig interpolants_.

####  3.2.1 Craig Interpolation

Given two formulas $A$ and $B$, if $A\Rightarrow B$, Craig’s interpolation
theorem [17] assures the existence of a formula $\tau$ such that
$A\Rightarrow\tau$ and $\tau\Rightarrow B$ are valid, and $\tau$ only involves
variables appearing in both $A$ and $B$. $\tau$ is called an _interpolant_ of
$A$ and $B$ as it is logically between $A$ and $B$. In the model-checking
community, Craig’s interpolation theorem is usually stated in the equivalent
form below.

###### Theorem 3.1

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$.

####  3.2.2 Computational Stages in IMC

IMC [11] has two nested stages in its computation: The outer stage unrolls a
state-transition system and poses BMC queries to satisfiability solvers; the
inner stage derives Craig interpolants and constructs fixed points. In the
following, we name the outer stage _BMC stage_ and the inner stage
_interpolation stage_.

In the BMC stage, a state-transition system is unfolded into several copies,
which is controlled by an unrolling counter. Suppose the value of the counter
is $k$. A BMC query depicting all possible paths from an initial state to a
property-violating state via at most $k$ transitions is posed:

$\displaystyle\underbrace{I(s_{0})T(s_{0},s_{1})}_{\text{$A(s_{0},s_{1})$}}\underbrace{T(s_{1},s_{2})\ldots
T(s_{k-1},s_{k})(\neg P(s_{1})\lor\ldots\lor\neg
P(s_{k}))}_{\text{$B(s_{1},s_{2},\ldots,s_{k})$}}.$ (2)

In the above formula, variable $s_{i}$ denotes the state after the $i$-th
transition. If Eq. 2 is satisfiable, a feasible counterexample to the safety
property is found. Otherwise, IMC enters the interpolation stage.

In the interpolation stage, a BMC query such as Eq. 2 is partitioned into two
formulas $A$ and $B$. According to Theorem 3.1, an interpolant
$\tau_{1}(s_{1})$ for Eq. 2 exists such that:

$\displaystyle I(s_{0})T(s_{0},s_{1})\rightarrow\tau_{1}(s_{1})\text{~{}is
valid and}$
$\displaystyle\tau_{1}(s_{1})\land\bigwedge_{i=1}^{k-1}T(s_{i},s_{i+1})\land\bigvee_{i=1}^{k}\neg
P(s_{i})\text{ is unsatisfiable.}$

Conceptually, $\tau_{1}(s_{1})$ summarizes the reason why Eq. 2 is
unsatisfiable: It overapproximates the set of states that are (1) reachable
via one transition from an initial state and (2) do not violate the safety
property within $(k-1)$ transitions.

A fixed point of the state-transition system may be constructed by computing
such interpolants iteratively. Substituting variable $s_{0}$ into $\tau_{1}$
and replacing the initial states $I(s_{0})$ in Eq. 2 by $\tau_{1}(s_{0})$, the
interpolation stage of IMC poses another BMC query from the first interpolant
$\tau_{1}$:

$\displaystyle\underbrace{\tau_{1}(s_{0})T(s_{0},s_{1})}_{\text{$A^{\prime}(s_{0},s_{1})$}}\underbrace{T(s_{1},s_{2})\ldots
T(s_{k-1},s_{k})(\neg P(s_{1})\lor\ldots\lor\neg
P(s_{k}))}_{\text{$B^{\prime}(s_{1},s_{2},\ldots,s_{k})$}}$

If the formula is still unsatisfiable, a second interpolant $\tau_{2}(s_{1})$
can be derived, which overapproximates the set of states reachable from an
initial state via two transitions. Replacing $\tau_{1}$ with $\tau_{2}$, one
can derive the next interpolant $\tau_{3}$ if the BMC query starting from
$\tau_{2}$ is again unsatisfiable. Suppose the above process is repeated $n$
times, and a list of interpolants $\tau_{1},\tau_{2},\ldots,\tau_{n}$ is
derived. Upon the derivation of the newest interpolant $\tau_{n}$, IMC
performs a _fixed-point check_ to decide whether a fixed point has been
reached: If $\tau_{n}$ is contained in the union of the initial states and
previous interpolants, namely, $\tau_{n}\Rightarrow
I\lor\bigvee_{j=1}^{n-1}\tau_{j}$ holds, the set
$I\lor\bigvee_{j=1}^{n-1}\tau_{j}$ is an inductive invariant of the system
[11]. The inductive invariant is also safe because every interpolant does not
violate the safety property according to the second condition of Theorem 3.1.
As a result, IMC concludes the system preserves the safety property.

If a BMC query starting from an interpolant is satisfiable, the safety
property is not definitely violated. The corresponding error path might be
spurious because the interpolant could involve unreachable states. In this
situation, IMC will return to the BMC stage and increment the unrolling
counter to confirm the existence of a feasible error path.

##  4 Augmenting IMC with Auxiliary Invariants

We propose two methods to augment IMC with auxiliary invariants. The first one
strengthens the fixed-point checks, and the second one strengthens the
interpolants derived in the interpolation stage. Given a state-transition
system $M=(I(s),T(s,s^{\prime}))$, we further assume that auxiliary invariants
are inductive. In other words, an invariant $Inv(s)$ satisfies
$I(s)\Rightarrow Inv(s)$ and $Inv(s)\land T(s,s^{\prime})\Rightarrow
Inv(s^{\prime})$. This assumption is reasonable in practice because invariant
generators, such as those based on data-flow analysis, usually perform a
fixed-point iteration and produce inductive invariants.

###  4.1 Approach 1: Strengthening Fixed-Point Checks

The first approach strengthens fixed-point checks by restricting the newest
interpolant with an auxiliary invariant. Let $\tau_{1},\ldots,\tau_{n}$ be a
list of interpolants derived in the interpolation stage. Instead of checking
$\tau_{n}\Rightarrow I\lor\bigvee_{j=1}^{n-1}\tau_{j}$, we strengthen the
check to $Inv\land\tau_{n}\Rightarrow I\lor\bigvee_{j=1}^{n-1}\tau_{j}$. The
intuition is to confine the scope of fixed-point checks mainly within
reachable states of the system such that the union of the initial states and
previous interpolants is more likely to contain the newest interpolant. The
correctness of this approach is stated in Theorem 4.1.

###### Theorem 4.1

Given a state-transition system $M=(I(s),T(s,s^{\prime}))$ and a safety
property $P(s)$, let $\tau_{1},\ldots,\tau_{n}$ be a list of interpolants
derived in the interpolation stage of IMC. If the strengthened fixed-point
check $Inv\land\tau_{n}\Rightarrow I\lor\bigvee_{j=1}^{n-1}\tau_{j}$ holds for
some auxiliary invariant $Inv$, $M$ fulfills the safety property $P(s)$.

###### Proof

We rely on the criterion described by Eq. 1 to show that $M$ fulfills $P$.
Defining $G$ to be $I\lor\bigvee_{j=1}^{n-1}\tau_{j}$, we will prove that $G$
satisfies Eq. 1.

Proving $I\Rightarrow G$ is trivial, and Theorem 3.1 guarantees that
$\tau_{1},\ldots,\tau_{n}$ do not violate the safety property, which assures
that $G\Rightarrow P$ holds.

To show $Inv(s)\land G(s)\land T(s,s^{\prime})\Rightarrow G(s^{\prime})$ is
valid, recall $I(s)\land T(s,s^{\prime})\Rightarrow\tau_{1}(s^{\prime})$ and
$\tau_{j}(s)\land T(s,s^{\prime})\Rightarrow\tau_{j+1}(s^{\prime})$ for
$j=1,\ldots,n-1$ are valid according to Theorem 3.1. Combining these
conditions and the inductiveness of the auxiliary invariant $Inv$, we simplify
the implication to

$\displaystyle Inv(s)\land(I(s)\lor\bigvee_{j=1}^{n-1}\tau_{j}(s))\land
T(s,s^{\prime})\Rightarrow
Inv(s^{\prime})\land(\bigvee_{j=1}^{n-1}\tau_{j}(s^{\prime})\lor\tau_{n}(s^{\prime})).$

Since the strengthened fixed-point check $Inv\land\tau_{n}\Rightarrow
I\lor\bigvee_{j=1}^{n-1}\tau_{j}$ holds, the right-hand side of the above
implication further implies
$(Inv(s^{\prime})\land\bigvee_{j=1}^{n-1}\tau_{j}(s^{\prime}))\lor(I(s^{\prime})\lor\bigvee_{j=1}^{n-1}\tau_{j}(s^{\prime}))$,
which equals $G(s^{\prime})$.

Therefore, we proved that $G$ satisfies Eq. 1, and hence $M$ fulfills $P$.

###  4.2 Approach 2: Strengthening Interpolants

The second approach strengthens interpolants by conjoining them with an
auxiliary invariant. Unlike the first approach, which only restricts the
newest interpolant with an auxiliary invariant in a fixed-point check, the
second approach replaces the original interpolants returned by the
interpolation procedure with the strengthened ones. That is, given a BMC query
starting from the initial states $I$ or a previously strengthened interpolant
$\tau_{j}\land Inv$, the interpolant $\tau_{j+1}$ is replaced by
$\tau_{j+1}\land Inv$. Note that if interpolants are strengthened, fixed-point
checks are effectively strengthened as well. Theorem 4.2 states that
$\tau_{j+1}\land Inv$ is also an interpolant for the BMC query, and hence the
correctness of the approach follows from the plain IMC algorithm.

###### Theorem 4.2

Given a transition system $M=(I(s),T(s,s^{\prime}))$ and a safety property
$P(s)$, consider an unsatisfiable BMC query $\lambda(s_{0})\land
T(s_{0},s_{1})\land\ldots\land T(s_{k-1},s_{k})\land\bigvee_{i=1}^{k}\neg
P(s_{i})$ posed in the interpolation stage of IMC, where $\lambda(s_{0})$ is
either $I(s_{0})$ or a previously strengthened interpolant
$\tau_{j}(s_{0})\land Inv(s_{0})$. Suppose $\tau_{j+1}(s_{1})$ is an
interpolant of the BMC query with $\lambda(s_{0})\land T(s_{0},s_{1})$ labeled
as formula $A$ and $T(s_{1},s_{2})\land\ldots\land
T(s_{k-1},s_{k})\land\bigvee_{i=1}^{k}\neg P(s_{i})$ labeled as formula $B$.
Then $\tau_{j+1}(s_{1})\land Inv(s_{1})$ is also an interpolant of the BMC
query.

###### Proof

To prove that $\tau_{j+1}(s_{1})\land Inv(s_{1})$ is also an interpolant, we
have to show that it satisfies the three conditions in Theorem 3.1. Namely,
(1) $\lambda(s_{0})\land T(s_{0},s_{1})\Rightarrow\tau_{j+1}(s_{1})\land
Inv(s_{1})$ is valid; (2) $\tau_{j+1}(s_{1})\land Inv(s_{1})\land
T(s_{1},s_{2})\land\ldots\land T(s_{k-1},s_{k})\land\bigvee_{i=1}^{k}\neg
P(s_{i})$ is unsatisfiable; and (3) $\tau_{j+1}(s_{1})\land Inv(s_{1})$ only
refers to the common variables of formulas $A$ and $B$. Condition (2) holds
because $\tau_{j+1}(s_{1})\land T(s_{1},s_{2})\land\ldots\land
T(s_{k-1},s_{k})\land\bigvee_{i=1}^{k}\neg P(s_{i})$ is already unsatisfiable
according to Theorem 3.1. Condition (3) holds because $\tau_{j+1}(s_{1})\land
Inv(s_{1})$ only uses the common variable $s_{1}$. In the following, we prove
condition (1) by splitting into two cases.

When $\lambda(s_{0})=I(s_{0})$, our proof goal is $I(s_{0})\land
T(s_{0},s_{1})\Rightarrow\tau_{j+1}(s_{1})\land Inv(s_{1})$. Applying Theorem
3.1 to $\tau_{j+1}$, we have $I(s_{0})\land
T(s_{0},s_{1})\Rightarrow\tau_{j+1}(s_{1})$. Since $Inv$ is an invariant and
hence contains all reachable states, we also have $I(s_{0})\land
T(s_{0},s_{1})\Rightarrow Inv(s_{1})$. Therefore, our proof goal is achieved.

When $\lambda(s_{0})=\tau_{j}(s_{0})\land Inv(s_{0})$, our proof goal is
$\tau_{j}(s_{0})\land Inv(s_{0})\land
T(s_{0},s_{1})\Rightarrow\tau_{j+1}(s_{1})\land Inv(s_{1})$. Applying Theorem
3.1 to $\tau_{j+1}$, we have $\tau_{j}(s_{0})\land Inv(s_{0})\land
T(s_{0},s_{1})\Rightarrow\tau_{j+1}(s_{1})$. Since $Inv$ is inductive, we also
have $Inv(s_{0})\land T(s_{0},s_{1})\Rightarrow Inv(s_{1})$. Our goal follows
from the two implications.

As both cases are proved, we conclude that $\tau_{j+1}(s_{1})\land Inv(s_{1})$
is also an interpolant of the BMC query and can be used in the interpolation
stage of IMC.

###  4.3 Comparison between the Two Approaches

The design spirit behind the two approaches is to make IMC capable of proving
the safety of a system with fewer iterations in the BMC and interpolation
stages. We attain this objective with the help of auxiliary invariants. In the
first approach, instead of an inductive invariant, IMC generates a relatively
inductive set of states, which might require fewer interpolation calls to
produce. In the second approach, in addition to strengthening fixed-point
checks, strengthened interpolants also make BMC queries in the interpolation
stage easier to be unsatisfiable. That is, IMC will remain in the
interpolation stage more often, searching for a proof of the safety property.
The second approach is more “aggressive” than the first one because
strengthened interpolants will change the interpolants obtained later, and IMC
will follow a different computational footprint. By contrast, the interpolants
encountered in the first approach are identical to the plain IMC algorithm if
the interpolation procedure is the same. Moreover, the first approach can in
principle be adopted by other verification algorithms with similar fixed-point
checks, whereas the second approach is specifically tailored towards IMC. In
our evaluation, we also experimented with a basic injection approach that
conjoins the safety property with auxiliary invariants. However, this approach
performed roughly the same as the plain IMC algorithm.

###  4.4 Augmented IMC Procedure

Algorithm 1 Augmenting IMC [30] with Auxiliary Invariants

0: a state-transition system $M=(I(s),T(s,s^{\prime}))$, a safety property
$P(s)$,an upper bound $k_{max}$ for the unrolling counter $k$,a Boolean flag
$\mathit{strengthen\\_fpc}$ to enable strengthening fixed-point checks, anda
Boolean flag $\mathit{strengthen\\_itp}$ to enable strengthening interpolants

0: true if $M$ fulfills $P$; false if a feasible error path is found; unknown
otherwise

0: the unrolling counter $k$,the auxiliary invariant computed by an external
invariant generator $Inv(s)$,the candidate (relatively) inductive set $G(s)$,
the computed interpolant $\tau$, andthe two formulas $A(s_{0},s_{1})$ and
$B(s_{1},\ldots,s_{k})$ for interpolation

1: if $\mathsf{sat}$($I(s_{0})\land\lnot P(s_{0})$) then

2: return false

3: $k:=1$

4: $Inv(s):=\top$

5: while $k\leq k_{max}$ do

6: $G(s):=I(s)$

7: $A(s_{0},s_{1}):=I(s_{0})\land T(s_{0},s_{1})$

8:
$B(s_{1},\ldots,s_{k}):=\bigwedge_{i=1}^{k-1}T(s_{i},s_{i+1})\land(\bigvee_{i=1}^{k}\lnot
P(s_{i}))$

9: if $\mathsf{sat}$($A(s_{0},s_{1})\land B(s_{1},\ldots,s_{k})$) then

10: return false // BMC finds a feasible error path

11: if $\mathit{strengthen\\_fpc}\lor\mathit{strengthen\\_itp}$ then

12: $Inv(s):=\mathsf{get\\_auxiliary\\_invariant}()$

13: while $\lnot\mathsf{sat}$($A(s_{0},s_{1})\land B(s_{1},\ldots,s_{k})$) do

14:
$\tau(s_{1}):=\mathsf{get\\_interpolant}(A(s_{0},s_{1}),B(s_{1},\ldots,s_{k}))$

15: if $\mathit{strengthen\\_itp}$ then

16: $\tau(s):=Inv(s)\land\tau(s)$

17: if $\mathit{strengthen\\_fpc}$ then

18: if $\lnot\mathsf{sat}$($Inv(s)\land\tau(s)\land\lnot G(s)$) then

19: return true // $G$ is relatively inductive to $Inv$

20: else

21: if $\lnot\mathsf{sat}$($\tau(s)\land\lnot G(s)$) then

22: return true // $G$ is an inductive invariant

23: $G(s):=G(s)\lor\tau(s)$ // Add new states to $G$

24: $A(s_{0},s_{1}):=\tau(s_{0})\land T(s_{0},s_{1})$ // Start next BMC query
from new states

25: $k:=k+1$

26: return unknown

The proposed procedure to augment IMC with auxiliary invariants is summarized
in Alg. 1. It has two arguments $\mathit{strengthen\\_fpc}$ and
$\mathit{strengthen\\_itp}$ to enable the discussed strengthening of fixed-
point checks and interpolants, respectively, on top of the original IMC
algorithm. An auxiliary invariant $Inv(s)$ is injected into IMC at 12 if the
current BMC query is unsatisfiable. If $\mathit{strengthen\\_fpc}$ is true,
the first approach to strengthen fixed-point checks is performed at 18. If
$\mathit{strengthen\\_itp}$ is true, the second approach to strengthen
interpolants is performed at 16. Observe that fixed-point checks are also
strengthened if interpolants are strengthened: 18 and 21 are equivalent if the
derived interpolant $\tau$ at 14 is replaced by $Inv\land\tau$.

##  5 Implementation

To investigate whether invariant injection is helpful for IMC, we apply the
augmented IMC procedure in Alg. 1 to verify programs. The proposed algorithm
was implemented in CPAchecker [34], a software-verification framework for the
programming language C. We chose CPAchecker because it provides an
implementation [30] of the plain IMC algorithm. The IMC implementation
extracts transition relations from programs with _large-block encoding_ [47].
Error labels in a program are used to specify the negation of safety
properties. In addition to an IMC implementation, CPAchecker also has a
continuously-refining invariant generator based on intervals [33], which is
used to enhance k-induction [22]. Before continuing the discussion, we
emphasize that the proposed approaches discussed in Sect. 4 are independent of
the implementation framework and not limited to specific invariant generators.

CPAchecker is based on _configurable program analysis_ (CPA) [48], which
defines an abstract domain used in a program analysis. The plain IMC algorithm
is implemented using several CPAs, with one of them tracking path formulas
between program locations in its abstract states [49]. This CPA is configured
to perform large-block encoding, which constructs formulas for complete loop
unrollings as transition relations [30]. Thanks to its flexibility, it
underpins the implementations of other SMT-based algorithms in CPAchecker
[50], including predicate analysis, Impact, and k-induction. We will compare
the proposed algorithm to these techniques in Sect. 6.

The continuously-refining invariant generator in CPAchecker uses a CPA with an
abstract domain based on expressions over intervals [33]. Compared to methods
concerning single intervals only, it can represent complex ranges like the
disjunction and conjunction of intervals, e.g.,
$(x<5\lor{}x>7)\land{}(1\leq{}y\leq{}8)$. Its precision includes a set of
important variables and a maximum depth of expressions. The precision can be
dynamically adjusted during the analysis [51] to produce more refined
invariants.

Given a CPA and an initial abstract state, CPAchecker constructs a set of
reachable abstract states by iteratively processing states and computing their
abstract successors. To perform a specific algorithm, required information can
be collected from the abstract states. For example, IMC collects the path
formulas to assemble BMC queries and derive interpolants [30]. The interval-
based invariant generator outputs the union of expressions as invariants [33].
In our implementation, we run Alg. 1 and the invariant generator in parallel
and inject auxiliary invariants to augment IMC.

##  6 Evaluation

To understand the effects of the proposed invariant-injection approaches on
the proof-finding ability of IMC, we pose the following research questions:

  * •

Part 1: augmented IMC vs. plain IMC

    * –

RQ1: Can auxiliary invariants reduce the numbers of program unrollings and
interpolation queries?

    * –

RQ2: Can augmented IMC prove the correctness of additional programs?

    * –

RQ3: Can invariant injection improve the run-time efficiency?

  * •

Part 2: augmented IMC vs. other approaches and tools

    * –

RQ4: Can augmented IMC find more proofs than other SMT-based software-
verification algorithms in CPAchecker?

    * –

RQ5: Can augmented IMC find more proofs than other state-of-the-art software
verifiers?

###  6.1 Evaluated Approaches and Tools

To answer the above research questions, we evaluated the proposed invariant-
injection methods for IMC against (1) its plain version plus three other SMT-
based algorithms in the same verification framework CPAchecker [34] and (2)
two other state-of-the-art software verifiers.

The plain IMC algorithm was recently adopted to verify programs [30]. The
three other approaches in CPAchecker are predicate abstraction [12, 52],
Impact [13], and k-induction boosted by continuously-refined invariants [22],
whose characteristics were compared in a recent article on SMT-based software
verification [50]. All proposed methods and compared algorithms above are
implemented in the same framework, so the confounding variables are kept to a
minimum (identical frontend, program encodings, SMT solvers, etc.) to
facilitate the comparison of algorithmic differences. For invariant
generation, we used the continuously-refining data-flow analysis (DF) [33]
described in Sect. 5. The invariant generator can prove the safety properties
of some programs on its own. In our experiments, we ignored the answers
computed by DF because our goal is to study the effects of auxiliary
invariants on the main analyses, namely, IMC and k-induction. In the
following, we denote the injection of continuously-refined invariants
generated by DF into k-induction as
KI$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF, and the augmented IMC
algorithms with fixed-point checks and interpolants strengthened by auxiliary
invariants as IMCf$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF and
IMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF, respectively.

To reflect the state of the art on software verification and invariant
injection, we further compared our approaches to 2ls [23], which has a mature
implementation of k-induction boosted by auxiliary invariants, and Symbiotic
[53], which is based on symbolic execution and performs well in the Intl.
Competitions on Software Verification [54] (the overall winner in 2022).

###  6.2 Benchmark Set

Since our goal is to investigate whether auxiliary invariants can improve
IMC’s capability of delivering correctness proofs, we selected verification
tasks without known violation to their reachability-safety properties from the
2022 Intl. Competition on Software Verification (SV-COMP ’22) [35].
Furthermore, to concentrate the evaluation on hard programs, we excluded
trivial tasks with bounded numbers of loop iterations.333This was approximated
by excluding tasks solvable by BMC of CPAchecker. To keep the program
encodings consistent across all evaluated approaches in CPAchecker, we only
considered single-loop programs in our experiments because the IMC
implementation in CPAchecker needs to transform a multi-loop program into a
single-loop program as preprocessing [30]. However, this is not a limitation
of the proposed augmenting methods. The proposed methods can work on multi-
loop programs as well if a single-loop transformation [55, 56] is used. In
total, we collected $1\,623$ verification tasks, each of which contains a
single-loop program and challenging safety properties.

###  6.3 Experimental Setup

All experiments were conducted on machines using a 3.4 GHz CPU (Intel Xeon
E3-1230 v5) with 8 processing units and 33 GB of RAM. The operating system was
Ubuntu 22.04 (64 bit), using Linux 5.15 and OpenJDK 17.0.5. Each verification
task was limited to 4 CPU cores, $15\text{\,}\mathrm{m}\mathrm{i}\mathrm{n}$
of CPU time, and $15\text{\,}\mathrm{G}\mathrm{B}$ of RAM. In our evaluation,
we utilized the benchmarking framework BenchExec [57] to ensure
reproducibility of our results, and CPAchecker at revision 42901 of branch
imc-with-invariants. All SMT and interpolation queries in CPAchecker were
handled by MathSAT5 [58]. Since we want to observe IMC’s behavior in the
presence of auxiliary invariants, we limited the CPU time allocated to the
invariant generator to $2.5\text{\,}\mathrm{m}\mathrm{i}\mathrm{n}$ such that
IMC had enough time to perform its analysis. For the comparison to other
software verifiers, we downloaded 2ls and Symbiotic from the tool archives of
SV-COMP ’22 [59].

###  6.4 Results

####  6.4.1 RQ1: Reduction of program unrollings and interpolation queries

To understand whether the invariant-injection techniques could reduce the
numbers of program unrollings and interpolation queries required by plain IMC
to find a proof, we conducted a case study on
IMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF. As discussed in Sect.
4.3, IMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF derives different
interpolants from plain IMC and is supposed to exhibit distinct computational
behavior. We further identified 870 tasks for which DF was able to generate
non-trivial and inductive invariants444The trivial invariant $\top$ represents
the entire state space.  because trivial invariants provide no additional
information to help IMC. The scatter plots Fig. 2a and Fig. 2b show the
comparison of IMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF and IMC
on the 870 tasks on the numbers of program unrollings and interpolation
queries, respectively. A data point ($x$, $y$) in the plots means that there
is a task solvable by both IMC and
IMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF, and IMC (resp.
IMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF) requires $x$ (resp.
$y$) times of the indicated operation. The color of a data point shows the
number of tasks falling into this coordinate. Data points under the diagonal
represent the tasks for which
IMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF needed fewer
operations than plain IMC. Observe that
IMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF often required fewer
program unrollings and interpolation calls. For programs correctly proved by
both, our augmenting approach reduced the number of program unrollings in 35
tasks, and the number of interpolation calls in 56 tasks.

IMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DFIMCNumber of tasks

(a) Program unrollings

IMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DFIMCNumber of tasks

(b) Interpolation queries

Figure 2: Comparison of the numbers of program unrollings and interpolation
queries

Table 1 shows the tasks for which augmented IMC exhibited significant
performance improvement. Upon these tasks, plain IMC either ran into timeouts
or required considerably more run-time, whereas the augmented versions were
able to deliver proofs efficiently. Under each algorithm, the table lists the
verification result (solved or timeout), the numbers of program unrollings and
interpolation queries, wall-time, and interpolation time (the time spent on
all interpolation queries). Note that since plain IMC suffered from timeouts
in most of these tasks, the reported numbers of unrollings and interpolation
queries are lower bounds of the actual numbers required to compute proofs,
which could be much higher.

Table 1: Statistics of tasks with significant improvement (time unit: with two
significant digits; ✓ for solved, and – for timeout)

| IMC |  IMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF
---|---|---
Task | result | #unroll | #itp | wall-time | itp-time | result | #unroll | #itp | wall-time | itp-time
Problem03_label03 | – | $9$ | $50$ | $872.22865271708$ | $744.979$ | ✓ | $6$ | $11$ | $27.238232209114358$ | $12.961$
Problem03_label15 | – | $8$ | $54$ | $876.379350814037$ | $747.834$ | ✓ | $6$ | $11$ | $35.356361616868526$ | $19.451$
Problem03_label51 | – | $11$ | $57$ | $878.3521001820918$ | $753.434$ | ✓ | $6$ | $11$ | $24.287363136885688$ | $10.283$
benchmark37_conj | – | $318$ | $316$ | $892.0208312040195$ | $851.141$ | ✓ | $2$ | $2$ | $1.8257458130829036$ | $0.008$
pals_lcr-var-start | – | $12$ | $16$ | $875.1322450151201$ | $632.583$ | ✓ | $11$ | $24$ | $760.8478177771904$ | $479.382$
pals_lcr.4.ufo.UNB | ✓ | $12$ | $23$ | $198.25573511817493$ | $164.821$ | ✓ | $11$ | $16$ | $116.0566888100002$ | $91.702$
phases_2-2 | – | $2$ | $1$ | $898.6676160399802$ | $897.066$ | ✓ | $2$ | $2$ | $2.201416672905907$ | $0.057$
s3_srvr_1a.BV.c.cil | – | $65$ | $441$ | $885.0645597530529$ | $544.280$ | ✓ | $6$ | $13$ | $6.2615407118573785$ | $1.016$
s3_srvr_2a.BV.c.cil | – | $40$ | $290$ | $886.5472344069276$ | $793.493$ | ✓ | $36$ | $252$ | $635.0260343221016$ | $538.770$
s3_srvr_2a_alt.BV | – | $38$ | $278$ | $882.8717780259904$ | $776.454$ | ✓ | $20$ | $125$ | $71.68477753107436$ | $51.658$

| IMC |  IMCf$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF
---|---|---
Task | result | #unroll | #itp | wall-time | itp-time | result | #unroll | #itp | wall-time | itp-time
Problem03_label01 | ✓ | $10$ | $73$ | $654.156850613188$ | $472.896$ | ✓ | $7$ | $13$ | $37.46677428903058$ | $17.998$
Problem03_label03 | – | $9$ | $50$ | $872.22865271708$ | $744.979$ | ✓ | $7$ | $15$ | $85.67790243797936$ | $61.715$
Problem03_label04 | ✓ | $8$ | $53$ | $141.33076911582612$ | $102.077$ | ✓ | $6$ | $11$ | $17.948978120926768$ | $4.849$
Problem03_label11 | ✓ | $8$ | $55$ | $113.87224058085121$ | $82.201$ | ✓ | $6$ | $9$ | $17.427703568944708$ | $4.054$
Problem03_label12 | ✓ | $9$ | $59$ | $509.70322883711196$ | $345.975$ | ✓ | $9$ | $18$ | $80.8643268099986$ | $59.340$
Problem03_label15 | – | $8$ | $54$ | $876.379350814037$ | $747.834$ | ✓ | $7$ | $18$ | $107.30843193409964$ | $80.402$
Problem03_label19 | ✓ | $9$ | $59$ | $134.35687817796133$ | $107.946$ | ✓ | $6$ | $9$ | $22.799386984901503$ | $6.634$
Problem03_label51 | – | $11$ | $57$ | $878.3521001820918$ | $753.434$ | ✓ | $8$ | $16$ | $49.77535207592882$ | $32.453$
s3_srvr_1a.BV.c.cil | – | $65$ | $441$ | $885.0645597530529$ | $544.280$ | ✓ | $62$ | $422$ | $656.1564103758428$ | $391.957$
s3_srvr_2a.BV.c.cil | – | $40$ | $290$ | $886.5472344069276$ | $793.493$ | ✓ | $20$ | $123$ | $77.1594064598903$ | $56.020$

####  6.4.2 RQ2: Effectiveness of augmented IMC vs. plain IMC

We compared the number of proved tasks of augmented IMC versus plain IMC to
evaluate the effectiveness of the proposed invariant-injection approaches.
Table 2 summarizes the results on the 870 tasks with non-trivial invariants.
Observe that IMCf$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF and
IMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF solved more tasks than
plain IMC. Specifically,
IMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF (resp.
IMCf$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF) found proofs for 23
(resp. 6) tasks where plain IMC ran into timeouts. However, it was not able to
solve 13 (resp. 4) tasks proven by plain IMC, partially due to the extra time
spent on invariant generation (see Sect. 6.5 for more discussion). Overall,
IMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF (resp.
IMCf$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF) proved 10 (resp. 2)
additional tasks compared to plain IMC, and there were 16 tasks solvable by
IMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF but not by plain IMC
or DF. Although not extraordinary, the increase shows invariant injection can
improve the effectiveness of plain IMC.

Table 2: Summary of the results for plain vs. augmented IMC on 870 tasks with non-trivial auxiliary invariants Algorithm | IMC | IMCf$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF | IMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF
---|---|---|---
Proofs | $534$ | $536$ | $544$
Timeouts | $297$ | $295$ | $287$
Out of memory | $0$ | $0$ | $0$
Other inconclusive | $39$ | $39$ | $39$

To account for the randomness in SMT solving and interpolation, we repeated
our experiments with five different random seeds for the underlying SMT
solver. The results are shown in Fig. 3. Observe that
IMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF consistently found
more proofs than plain IMC with all five random seeds, which demonstrates the
robustness of the proposed invariant-injection approaches.

7426189165$400$$450$$500$$550$Random
seed#ProofsIMCIMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF

Figure 3: Numbers of proofs found by IMC and
IMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF using different random
seeds for SMT solving (default seed: 42)

$400$$450$$500$$550$$0$$200$$400$$600$$800$$1000$n-th fastest correct
resultCPU time
()IMCIMCf$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DFIMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF

(a) CPU time

$400$$450$$500$$550$$0$$200$$400$$600$$800$$1000$n-th fastest correct
resultWall-time
()IMCIMCf$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DFIMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF

(b) Walltime

Figure 4: Quantile plots comparing the run-time of plain and augmented IMC

$1$$10$$100$$1000$$1$$10$$100$$1000$IMCIMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DFBoth
solvedIMC TOIMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF TO

(a) Walltime ()

$1$$10$$100$$1000$$1$$10$$100$$1000$IMCIMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DFBoth
solvedIMC TOIMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF TO

(b) Interpolation time ()

Figure 5: Comparison of wall-time and interpolation time (TO stands for
timeout)

####  6.4.3 RQ3: Run-time efficiency of augmented IMC vs. plain IMC

Quantile plots comparing the CPU time and wall-time usage of IMC,
IMCf$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF, and
IMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF on the tasks with non-
trivial invariants are shown in Fig. 4a and Fig. 4b, respectively. A data
point ($x$, $y$) in the plots indicates that $x$ tasks were correctly solved
by the respective algorithm within a time bound of $y$ seconds. To focus on
the performance differences for difficult tasks, we crop the first $400$ tasks
from the figures because they can be solved within
$1\text{\,}\mathrm{m}\mathrm{i}\mathrm{n}$. From Fig. 4a, observe that IMC
dominated its two augmented variants when the CPU time was below
$400\text{\,}\mathrm{s}$ because it does not have a parallel invariant
generator to consume extra time. However, as the elapsed CPU time increased,
IMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF took over and became
the best among the three. By contrast, Fig. 4b shows a clear advantage of
IMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF regarding the wall-
time consumption. It was able to solve the most tasks when the elapsed wall-
time was beyond $200\text{\,}\mathrm{s}$. In addition, although
IMCf$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF did not not perform as
well as IMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF on these
tasks, it still showed some wall-time improvement over plain IMC. The results
indicate that our proposed augmenting approaches can not only prove the
correctness of additional programs but also reduce the wall-time for solving
difficult tasks.

The scatter plots in Fig. 5 compare the wall-time and interpolation time
consumed by IMC and IMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF on
the tasks with non-trivial invariants. A data point ($x$, $y$) in the plots
indicates a task that can be solved by IMC or
IMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF, for which the former
took $x$ amount of wall-time (resp. interpolation time), and the latter took
$y$ amount of wall-time (resp. interpolation time). Observe that invariant
injection helps to improve plain IMC’s wall-time efficiency for time-consuming
tasks because more data points are below the diagonal in the top-right quarter
of Fig. 5a. As for interpolation, invariant injection generally lowered the
summation of time spent on all queries, as can be seen from Fig. 5b. Moreover,
there were 20 tasks showing an order of magnitude reduction.

####  6.4.4 RQ4: Comparison with other SMT-based methods in CPAchecker

Table 3: Summary of the results for IMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF vs. other SMT-based algorithms in CPAchecker, 2ls, and Symbiotic, on all $1\,623$ tasks Tool | CPAchecker | 2ls | Symbiotic
---|---|---|---
Algorithm | IMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF | KI$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF | Impact | PredAbs | - | -
Proofs | $871$ | $631$ | $801$ | $780$ | $556$ | $319$
Timeouts | $542$ | $707$ | $618$ | $712$ | $675$ | $710$
Out of memory | $110$ | $237$ | $75$ | $11$ | $64$ | $324$
Other inconclusive | $100$ | $48$ | $129$ | $120$ | $328$ | $270$

$0$$200$$400$$600$$800$$0.1$$1$$10$$100$$1000$n-th fastest correct resultWall-
time ()IMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF
(CPA)KI$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF (CPA)Impact
(CPA)PredAbs (CPA)2lsSymbiotic

Figure 6: Quantile plot comparing
IMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF with other approaches
and tools

To study whether the the proposed invariant-injection approaches for IMC could
deliver more proofs than other SMT-based methods in CPAchecker, we evaluated
IMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF against
KI$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF [22], Impact [13], and
predicate abstraction (PredAbs) [52, 12].555Plain IMC has been compared with
other approaches in a technical report [30]. The results are summarized in
Table 3, where IMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF solved
the most tasks among the compared algorithms. Figure 6 shows the quantile plot
of the wall-time usage for each compared algorithm.
IMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF outperformed other
polished SMT-based approaches in CPAchecker in terms of both the number of
solved tasks and the run-time efficiency. There were 324, 88, and 143
additional tasks solvable by
IMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF, but not by
KI$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF, Impact, and predicate
abstraction, respectively. In total,
IMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF uniquely solved 10
tasks among the compared algorithms in CPAchecker, demonstrating our
contribution to SMT-based software verification.

####  6.4.5 RQ5: Comparison with other software verifiers

Table 3 and Fig. 6 also report the results for 2ls [23] and Symbiotic [53]
(executed with the configurations used in SV-COMP ’22), and our proposed
method IMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF found
significantly more proofs than both of them. In particular, 423 and 624
additional tasks were solved by
IMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF, but not by 2ls and
Symbiotic, respectively, and a total of 342 tasks were uniquely solved by
IMCi$\,\boldsymbol{\circlearrowleft}$$\longleftarrow$DF. The results
demonstrate the value of our invariant-injection methods for IMC and justify
our contribution to the state of the art of software model checking.

###  6.5 Discussion

In general, strengthened interpolants help to decrease Our goal is to study
whether invariant injection is helpful for IMC, and the experimental results
reported above confirm its usefulness. In our experiments, strengthened
interpolants helped decrease the number of interpolation queries (Fig. 2b) and
the total interpolation time (Fig. 5b), but the effect came at a price: SMT
and interpolation queries may become more challenging. There were several
tasks solvable by plain IMC in a minute but stuck at one difficult SMT query
with a strengthened interpolant for hundreds of seconds. This phenomenon is an
overhead against the performance of augmented IMC. In principle, one could
limit the time spent on a call for SMT solving or interpolation and fall back
to the original interpolant if the strengthened one makes the query too time-
consuming. Nevertheless, it is not straightforward to reuse an SMT solver
stack after it receives a timeout signal because most solvers do not specify
their behavior in this situation. To summarize, the effects of invariant
injection on IMC are mixed: On one hand, it reduces the numbers of unrollings
and interpolation calls; on the other hand, each SMT or interpolation query
might consume more time. A similar trade-off between fewer refinement steps
and extra computation effort to achieve the reduction was reported for the
verifier Ufo [44]. In our evaluation, we observed a clear decrease in the
numbers of unrollings and interpolation calls, but the number of solved tasks
did not increase remarkably. Similar observations that the run-time does not
necessarily benefit from auxiliary invariants and that the number of solved
tasks might not increase significantly have also been reported in previous
publications [32, 23] on invariant-aided verification.

##  7 Conclusion

We augmented IMC, an interpolation-based model-checking algorithm published by
McMillan in 2003 [11], via injecting auxiliary invariants to reduce the
numbers of program unrollings and interpolation queries needed to prove the
correctness of programs. Invariants are used to strengthen (1) the checks for
determining whether a fixed point is reached, or (2) the interpolants derived
during the procedure. We rigorously proved the correctness of the proposed
approaches and implemented both techniques in the verification tool
CPAchecker. We empirically evaluated our implementations against four SMT-
based verification approaches in CPAchecker and two state-of-the-art software
verifiers over C programs whose safety properties are hard to prove. Our
experiments show that the proposed techniques effectively reduced the numbers
of program unrollings and interpolation calls and therefore reduced the wall-
time usage compared to plain IMC. Furthermore, the proposed augmentation of
IMC delivered more proofs than the compared SMT-based algorithms in CPAchecker
and solved 342 tasks unsolvable by the compared tools. As future work, to
mitigate the extra time spent on SMT solving or interpolation caused by
strengthened interpolants, we plan to devise a strategy to selectively inject
invariants into IMC only when they are more likely to be helpful, in order to
further improve the performance of the proposed methods.

####  7.0.1 Data-Availability Statement

To enhance the verifiability and transparency of the paper, all relevant
materials, including used tools, benchmark tasks, and raw experimental data,
are available in a supplemental reproduction package [60]. More information is
available at https://www.sosy-lab.org/research/imc-df/.

####  7.0.2 Funding Statement

This project was funded in part by the Deutsche Forschungsgemeinschaft (DFG) –
378803395 (ConVeY).

## References

  * [1] Beyer, D., Chien, P.C., Lee, N.Z.: Augmenting interpolation-based model checking with auxiliary invariants. In: Proc. SPIN (2024)
  * [2] Myers, G.J., Sandler, C., Badgett, T.: The Art of Software Testing. Wiley, 3rd edn. (2011). https://www.worldcat.org/isbn/978-1-119-20248-6
  * [3] Jhala, R., Majumdar, R.: Software model checking. ACM Computing Surveys 41(4) (2009). https://doi.org/10.1145/1592434.1592438
  * [4] Kildall, G.A.: A unified approach to global program optimization. In: Proc. POPL. pp. 194–206. ACM (1973). https://doi.org/10.1145/512927.512945
  * [5] Kam, J., Ullman, J.: Global data-flow analysis and iterative algorithms. J. ACM 23, 158–171 (1976). https://doi.org/10.1145/321921.321938
  * [6] Sharir, M., Pnueli, A.: Two approaches to interprocedural data-flow analysis. In: Program Flow Analysis: Theory and Applications. pp. 189–233. Prentice-Hall (1981). https://www.worldcat.org/isbn/978-0-137-29681-1
  * [7] Kennedy, K.: A survey of data-flow analysis techniques. In: Program Flow Analysis: Theory and Applications, pp. 5–54. Prentice Hall (1981). https://www.worldcat.org/isbn/978-0-137-29681-1
  * [8] Jones, N.D., Muchnick, S.S.: A flexible approach to interprocedural data-flow analysis and programs with recursive data structures. In: Proc. POPL. pp. 66–74. ACM (1982). https://doi.org/10.1145/582153.582161
  * [9] Ryder, B.G.: Incremental data-flow analysis. In: Proc. POPL. pp. 167–176. ACM (1983). https://doi.org/10.1145/567067.567084
  * [10] Reps, T.W., Horwitz, S., Sagiv, M.: Precise interprocedural data-flow analysis via graph reachability. In: Proc. POPL. pp. 49–61. ACM (1995). https://doi.org/10.1145/199448.199462
  * [11] McMillan, K.L.: Interpolation and SAT-based model checking. In: Proc. CAV. pp. 1–13. LNCS 2725, Springer (2003). https://doi.org/10.1007/978-3-540-45069-6_1
  * [12] Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Proc. POPL. pp. 232–244. ACM (2004). https://doi.org/10.1145/964001.964021
  * [13] McMillan, K.L.: Lazy abstraction with interpolants. In: Proc. CAV. pp. 123–136. LNCS 4144, Springer (2006). https://doi.org/10.1007/11817963_14
  * [14] Vizel, Y., Grumberg, O.: Interpolation-sequence based model checking. In: Proc. FMCAD. pp. 1–8. IEEE (2009). https://doi.org/10.1109/FMCAD.2009.5351148
  * [15] McMillan, K.L.: Lazy annotation for program testing and verification. In: Proc. CAV. pp. 104–118. LNCS 6174, Springer (2010). https://doi.org/10.1007/978-3-642-14295-6_10
  * [16] Cimatti, A., Griggio, A.: Software model checking via IC3. In: Proc. CAV. pp. 277–293. LNCS 7358, Springer (2012). https://doi.org/10.1007/978-3-642-31424-7_23
  * [17] Craig, W.: Linear reasoning. A new form of the Herbrand-Gentzen theorem. J. Symb. Log. 22(3), 250–268 (1957). https://doi.org/10.2307/2963593
  * [18] Awedh, M., Somenzi, F.: Automatic invariant strengthening to prove properties in bounded model checking. In: Proc. DAC. pp. 1073–1076. ACM (2006). https://doi.org/10.1145/1146909.1147180
  * [19] Ganai, M.K., Gupta, A.: Accelerating high-level bounded model checking. In: Proc. ICCAD. pp. 794–801. ACM (2006). https://doi.org/10.1145/1233501.1233664
  * [20] Cheng, X., Hsiao, M.S.: Simulation-directed invariant mining for software verification. In: Proc. DATE. pp. 682–687. ACM (2008). https://doi.org/10.1109/DATE.2008.4484757
  * [21] Donaldson, A.F., Haller, L., Kröning, D.: Strengthening induction-based race checking with lightweight static analysis. In: Proc. VMCAI. pp. 169–183. LNCS 6538, Springer (2011). https://doi.org/10.1007/978-3-642-18275-4_13
  * [22] Beyer, D., Dangl, M., Wendler, P.: Boosting k-induction with continuously-refined invariants. In: Proc. CAV. pp. 622–640. LNCS 9206, Springer (2015). https://doi.org/10.1007/978-3-319-21690-4_42
  * [23] Brain, M., Joshi, S., Kröning, D., Schrammel, P.: Safety verification and refutation by k-invariants and k-induction. In: Proc. SAS. pp. 145–161. LNCS 9291, Springer (2015). https://doi.org/10.1007/978-3-662-48288-9_9
  * [24] Rocha, H., Ismail, H.I., Cordeiro, L.C., Barreto, R.S.: Model checking embedded C software using k-induction and invariants. In: Proc. SBESC. pp. 90–95. IEEE (2015). https://doi.org/10.1109/SBESC.2015.24
  * [25] Jovanovic, D., Dutertre, B.: Property-directed k-induction. In: Proc. FMCAD. pp. 85–92. IEEE (2016). https://doi.org/10.1109/FMCAD.2016.7886665
  * [26] Fischer, J., Jhala, R., Majumdar, R.: Joining data flow with predicates. In: Proc. FSE. pp. 227–236. ACM (2005). https://doi.org/10.1145/1081706.1081742
  * [27] Jain, H., Ivancic, F., Gupta, A., Shlyakhter, I., Wang, C.: Using statically computed invariants inside the predicate abstraction and refinement loop. In: Proc. CAV. pp. 137–151. LNCS 4144, Springer (2006). https://doi.org/10.1007/11817963_15
  * [28] Pasareanu, C.S., Visser, W.: Verification of Java programs using symbolic execution and invariant generation. In: Proc. SPIN. pp. 164–181. LNCS 2989, Springer (2004). https://doi.org/10.1007/978-3-540-24732-6_13
  * [29] Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Proc. CAV. pp. 343–361. LNCS 9206, Springer (2015). https://doi.org/10.1007/978-3-319-21690-4_20
  * [30] Beyer, D., Lee, N.Z., Wendler, P.: Interpolation and SAT-based model checking revisited: Adoption to software verification. arXiv/CoRR 2208(05046) (July 2022). https://doi.org/10.48550/arXiv.2208.05046
  * [31] Case, M.L., Mishchenko, A., Brayton, R.K.: Automated extraction of inductive invariants to aid model checking. In: Proc. FMCAD. pp. 165–172 (2007). https://doi.org/10.1109/FAMCAD.2007.12
  * [32] Cabodi, G., Nocco, S., Quer, S.: Strengthening model checking techniques with inductive invariants. IEEE Trans. on CAD of Integrated Circuits and Systems 28(1), 154–158 (2009). https://doi.org/10.1109/TCAD.2008.2009147
  * [33] Beyer, D., Chien, P.C., Lee, N.Z.: CPA-DF: A tool for configurable interval analysis to boost program verification. In: Proc. ASE. pp. 2050–2053. IEEE (2023). https://doi.org/10.1109/ASE56229.2023.00213
  * [34] Beyer, D., Keremoglu, M.E.: CPAchecker: A tool for configurable software verification. In: Proc. CAV. pp. 184–190. LNCS 6806, Springer (2011). https://doi.org/10.1007/978-3-642-22110-1_16
  * [35] Beyer, D.: Progress on software verification: SV-COMP 2022. In: Proc. TACAS (2). pp. 375–402. LNCS 13244, Springer (2022). https://doi.org/10.1007/978-3-030-99527-0_20
  * [36] Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Global value numbers and redundant computations. In: Proc. POPL. pp. 12–27. ACM (1988). https://doi.org/10.1145/73560.73562
  * [37] Bodik, R., Anik, S.: Path-sensitive value-flow analysis. In: Proc. POPL. pp. 237–251. ACM (1998). https://doi.org/10.1145/268946.268966
  * [38] Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proc. Int. Symp. on Programming. pp. 106–130. Dunod (1976). https://www.di.ens.fr/~cousot/COUSOTpapers/publications.www/CousotCousot-ISOP-76-Dunod-p106--130-1976.pdf
  * [39] Bradley, A.R., Manna, Z.: Property-directed incremental invariant generation. Formal Asp. Comput. 20(4-5), 379–405 (2008). https://doi.org/10.1007/s00165-008-0080-9
  * [40] Bradley, A.R.: SAT-based model checking without unrolling. In: Proc. VMCAI. pp. 70–87. LNCS 6538, Springer (2011). https://doi.org/10.1007/978-3-642-18275-4_7
  * [41] Fedyukovich, G., Bodík, R.: Accelerating syntax-guided invariant synthesis. In: Proc. TACAS. pp. 251–269. LNCS 10805, Springer (2018). https://doi.org/10.1007/978-3-319-89960-2_14
  * [42] Beyer, D., Dangl, M.: Software verification with PDR: An implementation of the state of the art. In: Proc. TACAS (1). pp. 3–21. LNCS 12078, Springer (2020). https://doi.org/10.1007/978-3-030-45190-5_1
  * [43] Kahsai, T., Tinelli, C.: PKind: A parallel k-induction based model checker. In: Proc. Int. Workshop on Parallel and Distributed Methods in Verification. pp. 55–62. EPTCS 72, EPTCS (2011). https://doi.org/10.4204/EPTCS.72.6
  * [44] Albarghouthi, A., Li, Y., Gurfinkel, A., Chechik, M.: Ufo: A framework for abstraction- and interpolation-based software verification. In: Proc. CAV, pp. 672–678. LNCS 7358, Springer (2012). https://doi.org/10.1007/978-3-642-31424-7_48
  * [45] Komuravelli, A., Gurfinkel, A., Chaki, S., Clarke, E.M.: Automatic abstraction in SMT-based unbounded software model checking. In: Proc. CAV. pp. 846–862. LNCS 8044, Springer (2013). https://doi.org/10.1007/978-3-642-39799-8_59
  * [46] Brat, G., Navas, J.A., Shi, N., Venet, A.: Ikos A framework for static analysis based on abstract interpretation. In: Proc. SEFM. pp. 271–277. LNCS 8702, Springer (2014). https://doi.org/10.1007/978-3-319-10431-7_20
  * [47] Beyer, D., Cimatti, A., Griggio, A., Keremoglu, M.E., Sebastiani, R.: Software model checking via large-block encoding. In: Proc. FMCAD. pp. 25–32. IEEE (2009). https://doi.org/10.1109/FMCAD.2009.5351147
  * [48] Beyer, D., Henzinger, T.A., Théoduloz, G.: Configurable software verification: Concretizing the convergence of model checking and program analysis. In: Proc. CAV. pp. 504–518. LNCS 4590, Springer (2007). https://doi.org/10.1007/978-3-540-73368-3_51
  * [49] Beyer, D., Keremoglu, M.E., Wendler, P.: Predicate abstraction with adjustable-block encoding. In: Proc. FMCAD. pp. 189–197. FMCAD (2010). https://ieeexplore.ieee.org/document/5770949
  * [50] Beyer, D., Dangl, M., Wendler, P.: A unifying view on SMT-based software verification. J. Autom. Reasoning 60(3), 299–335 (2018). https://doi.org/10.1007/s10817-017-9432-6
  * [51] Beyer, D., Henzinger, T.A., Théoduloz, G.: Program analysis with dynamic precision adjustment. In: Proc. ASE. pp. 29–38. IEEE (2008). https://doi.org/10.1109/ASE.2008.13
  * [52] Graf, S., Saïdi, H.: Construction of abstract state graphs with Pvs. In: Proc. CAV. pp. 72–83. LNCS 1254, Springer (1997). https://doi.org/10.1007/3-540-63166-6_10
  * [53] Slabý, J., Strejček, J., Trtík, M.: Checking properties described by state machines: On synergy of instrumentation, slicing, and symbolic execution. In: Proc. FMICS. pp. 207–221. LNCS 7437, Springer (2012). https://doi.org/10.1007/978-3-642-32469-7_14
  * [54] Beyer, D.: Competition on software verification and witness validation: SV-COMP 2023. In: Proc. TACAS (2). pp. 495–522. LNCS 13994, Springer (2023). https://doi.org/10.1007/978-3-031-30820-8_29
  * [55] Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison-Wesley (1986). https://www.worldcat.org/isbn/978-0-201-10088-4
  * [56] Donaldson, A.F., Kröning, D., Rümmer, P.: Automatic analysis of DMA races using model checking and _k_ -induction. FMSD 39(1), 83–113 (2011). https://doi.org/10.1007/s10703-011-0124-2
  * [57] Beyer, D., Löwe, S., Wendler, P.: Reliable benchmarking: Requirements and solutions. Int. J. Softw. Tools Technol. Transfer 21(1), 1–29 (2019). https://doi.org/10.1007/s10009-017-0469-y
  * [58] Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Proc. TACAS. pp. 93–107. LNCS 7795, Springer (2013). https://doi.org/10.1007/978-3-642-36742-7_7
  * [59] Beyer, D.: Verifiers and validators of the 11th Intl. Competition on Software Verification (SV-COMP 2022). Zenodo (2022). https://doi.org/10.5281/zenodo.5959149
  * [60] Beyer, D., Chien, P.C., Lee, N.Z.: Reproduction package for SPIN 2024 submission ‘augmenting interpolation-based model checking with auxiliary invariants’. Zenodo (2024). https://doi.org/10.5281/zenodo.10548594