Dynamically Detecting Likely Program Invariants

Abstract

Explicitly stated program invariants can help programmers by characterizing certain aspects of program execution and identifying program properties that must be preserved when modifying code. In practice, these invariants are usually absent from code. An alternative to expecting programmers to annotate code with invariants is to automatically infer invariants from the program itself. This talk describes dynamic techniques for discovering invariants from execution traces; the essential idea is to look for patterns in and relationships among variable values over a set of executions. An implementation has indicated that the approach is both effective -- successfully rediscovering formal specifications -- and useful -- discovering invariants that assisted a software evolution task. A naive implementation of dynamic invariant inference suffers both from excessive runtime and also from reporting irrelevant invariants and failing to report relevant ones. I will discuss several improvements that together make the system usable: statistical confidence measures, eliminating unused polymorphism, suppressing redundant and coincidentally true properties, and limiting which variables are compared to one another. I will also show how to extend dynamic invariant inference to pointer-directed data structures, which requires traversal of data structures and discovery of conditional rather than universally true invariants. This is joint work with Jake Cockrell, Adam Czeisler, Bill Griswold, Josh Kataoka, and David Notkin.