skip to main content
Department of Computer Science University of Colorado Boulder
cu: home | engineering | mycuinfo | about | cu a-z | search cu | contact cu cs: about | calendar | directory | catalog | schedules | mobile | contact cs
home · events · colloquia · 1999-2000 · 

Colloquium - Ernst

ECCR 150

Dynamically Detecting Likely Program Invariants
Department of Computer Science, University of Washington

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.

Michael Ernst photo

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.

The Department holds colloquia throughout the Fall and Spring semesters. These colloquia, open to the public, are typically held on Thursday afternoons, but sometimes occur at other times as well. If you would like to receive email notification of upcoming colloquia, subscribe to our Colloquia Mailing List. If you would like to schedule a colloquium, see Colloquium Scheduling.

Sign language interpreters are available upon request. Please contact Stephanie Morris at least five days prior to the colloquium.

See also:
Department of Computer Science
College of Engineering and Applied Science
University of Colorado Boulder
Boulder, CO 80309-0430 USA
Send email to

Engineering Center Office Tower
ECOT 717
FAX +1-303-492-2844
XHTML 1.0/CSS2 ©2012 Regents of the University of Colorado
Privacy · Legal · Trademarks
May 5, 2012 (13:29)