Danger Invariants

TL;DR

This paper introduces danger invariants, a novel concept that combines the scalability of static analysis with the precision of bounded model checking to efficiently find deep bugs in programs.

Contribution

It proposes danger invariants as the dual to safety invariants, enabling bug detection without explicit loop unwinding, using second-order SAT solving.

Findings

Successfully applied danger invariants to complex programs from literature.

Achieved bug detection with high precision and scalability.

Demonstrated advantages over traditional static analyzers and BMC.

Abstract

Static analysers search for overapproximating proofs of safety commonly known as safety invariants. Fundamentally, such analysers summarise traces into sets of states, thus trading the ability to distinguish traces for computational tractability. Conversely, static bug finders (e.g. Bounded Model Checking) give evidence for the failure of an assertion in the form of a counterexample, which can be inspected by the user. However, static bug finders fail to scale when analysing programs with bugs that require many iterations of a loop as the computational effort grows exponentially with the depth of the bug. We propose a novel approach for finding bugs, which delivers the performance of abstract interpretation together with the concrete precision of BMC. To do this, we introduce the concept of danger invariants -- the dual to safety invariants. Danger invariants summarise sets of traces that are guaranteed to reach an error state. This summarisation allows us to find deep bugs without false alarms and without explicitly unwinding loops. We present a second-order formulation of danger invariants and use the Second-Order SAT solver described in previous work to compute danger invariants for intricate programs taken from the literature.