Repository logo
 

Danger Invariants

Accepted version
Peer-reviewed

Type

Conference Object

Change log

Authors

David, Cristina 
Kesseli, Pascal 
Kroening, Daniel 
Lewis, Matt 

Abstract

Static analysers search for overapproximating proofs of safety commonly known as safety invariants. Conversely, static bug finders (e.g. Bounded Model Checking) give evidence for the failure of an assertion in the form of a counterexample trace. As opposed to safety invariants, the size of a counterexample is dependent on the depth of the bug, i.e., the length of the execution trace prior to the error state, which also determines the computational effort required to find them. We propose a way of expressing danger proofs that is independent of the depth of bugs. Essentially, such danger proofs constitute a compact representation of a counterexample trace, which we call a danger invariant. Danger invariants summarise sets of traces that are guaranteed to be able to reach an error state. Our conjecture is that such danger proofs will enable the design of bug finding analyses for which the computational effort is independent of the depth of bugs, and thus find deep bugs more efficiently. As an exemplar of an analysis that uses danger invariants, we design a bug finding technique based on a synthesis engine. We implemented this technique and compute danger invariants for intricate programs taken from SV-COMP 2016.

Description

Keywords

46 Information and Computing Sciences, 4612 Software Engineering

Journal Title

FM 2016: Formal Methods - 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings

Conference Name

International Symposium on Formal Methods

Journal ISSN

0302-9743
1611-3349

Volume Title

Publisher

Springer International Publishing

Rights

All rights reserved