Speaker:  Michael Ernst
Affiliation:  University of Washington
Date:  February 15, 2000
Time & Place:  4:15 PM, B14 Hollister
Host:  Greg Morrisett
Title:  Dynamically Detecting Likely Program Invariants

Explicitly stated program invariants can help programmers by characterizing 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 approaches that together make the system usable: statistical confidence measures, ignoring unchanged values, suppressing implied invariants, limiting which variables are compared to one another, and eliminating unused polymorphism. 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.