home · mobile · calendar · colloquia · 1999-2000 · 

Colloquium - Ernst

Dynamically Detecting Likely Program Invariants
Department of Computer Science, University of Washington
2/24/2000
11:00am-12:15pm

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 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.

Department of Computer Science
University of Colorado Boulder
Boulder, CO 80309-0430 USA
webmaster@cs.colorado.edu
www.cs.colorado.edu
May 5, 2012 (14:13)
XHTML 1.0/CSS2
©2012