ABSTRACT. We present an automated compositional program verification technique
for safety properties based on \emph{conditional inductive
invariants}. For a given program part (e.g., a single loop) and a
postcondition $\varphi$, we show how to, using a Max-SMT solver, an
inductive invariant together with a precondition can be synthesized
so that the precondition ensures the validity of the invariant and
that the invariant implies $\varphi$. From this, we build a
bottom-up program verification framework that propagates
preconditions of small program parts as postconditions for preceding
program parts. The method recovers from failures to prove the
validity of a precondition, using the obtained intermediate results
to restrict the search space for further proof attempts.

As only small program parts need to be handled at a time, our method
is scalable and distributable. The derived conditions can be viewed
as implicit contracts between different parts of the program, and
thus enable an incremental program analysis.

ABSTRACT. Acceleration is a technique for summarising loops by computing a closed-form
representation of the loop behaviour. The closed form can be turned into an
\emph{accelerator}, which is a code snippet that skips over intermediate
states of the loop to the end of the loop in a single step.

Program analysers rely on invariant generation techniques to reason about
loops. The state-of-the-art invariant generation techniques, in practice,
often struggle to find concise loop invariants, and, instead, degrade into
unrolling loops, which is ineffective for non-trivial programs. In this
paper, we evaluate experimentally whether loop accelerators enable
\emph{existing} program analysis algorithm to discover loop invariants more
reliably and more efficiently. This paper is the first comprehensive study
on the synergies between acceleration and invariant generation. We report
our experience on several tools (UFO, CPAchecker, CBMC and Impara) with a
collection of safe and unsafe programs drawn from the Software Verification
Competition and the literature.

ABSTRACT. This paper presents a new method for automatically generating numerical invariants for imperative programs. Given a program, our procedure computes a binary input/output relation on program states which over-approximates the behaviour of the program. It is compositional in the sense that it operates by decomposing the program into parts, computing an abstract meaning of each part, and then composing the meanings. Our method for approximating loop behaviour is based on first approximating the meaning of the loop body, extracting recurrence relations from that approximation, and then using the closed forms to approximate the loop. Our experiments demonstrate that on verification tasks, our method is competitive with leading invariant generation and verification tools.

Theory-Aided Model Checking of Concurrent Transition Systems

SPEAKER: unknown

ABSTRACT. We present a method for the automatic compositional verification of certain classes of concurrent programs. Our approach is based on the casting of the model checking problem into a theory of transition systems within CVC4, a DPLL(T) based SMT solver. Our transition system theory then cooperates with other theories supported by the solver (e.g., arithmetic, arrays), which can help accelerate the verification process. More specifically, our theory solver looks for known patterns within the input programs and uses them to generate lemmas in the languages of other theories. When applicable, these lemmas can often steer the search away from safe parts of the search space, reducing the number of states to be explored and expediting the model checking procedure. We demonstrate the potential of our technique on a number of broad classes of programs.

Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays

SPEAKER: unknown

ABSTRACT. We present a compositional SMT-based algorithm for safety of procedural C
programs that takes the heap into consideration as well. Existing SMT-based
approaches are either largely restricted to handling linear arithmetic
operations and properties, or are non-compositional. We use Constrained Horn
Clauses (CHCs) to represent the verification conditions where the memory
operations are modeled using the extensional theory of arrays (ARR). First, we
describe an exponential time quantifier elimination (QE) algorithm for ARR which
can introduce new quantifiers of the index and value sorts. Second, we adapt the
QE algorithm to efficiently obtain under-approximations using models, resulting
in a polynomial time Model Based Projection (MBP) algorithm. Third, we integrate
the MBP algorithm into the framework of compositional reasoning of procedural
programs using may and must summaries recently proposed by us. Our solutions to
the CHCs are currently restricted to quantifier-free formulas. Finally,
we describe our practical experience over SV-COMP'15 benchmarks using an
implementation in the tool SPACER.

Difference Constraints: An adequate Abstraction for Complexity Analysis of Imperative Programs

SPEAKER: unknown

ABSTRACT. Difference constraints have been used for termination analysis in the literature, where they denote relational inequalities of the form $x' \le y + c$, and describe that the value of $x$ in the current state is at most the value of $y$ in the previous state plus some constant $c \in \mathbb{Z}$. In this paper, we argue that the complexity of imperative programs typically arises from counter increments and resets, which can be modeled naturally by difference constraints. We present the first practical algorithm for the analysis of difference constraint programs and describe how C programs can be abstracted to difference constraint programs. Our approach contributes to the field of automated complexity and (resource) bound analysis by enabling automated amortized complexity analysis for a new class of programs and providing a conceptually simple program model that relates invariant- and bound analysis. We demonstrate the effectiveness of our approach through a thorough experimental comparison on real world C code: our tool Loopus computes the complexity for considerably more functions in less time than related tools from the literature.