SHF:Small:Collaborative Research:Dynamic Invariant Inference, Enhanced

University Of Massachusetts Amherst, Amherst MA

Investigators

Abstract

In just a decade, dynamic invariant inference has emerged as one of the most promising directions in program analysis, with a variety of applications. An invariant inference system observes a program during test execution and filters a large number of candidate invariants (i.e., suspected relations between program data), finally reporting only those that hold with high confidence. However, inferred invariants are not always true (they depend on the quality of a test suite), and the few really useful invariants discovered are often accompanied by many more true but trivial and irrelevant facts. This work improves the quality of discovered invariants by ensuring their consistency with facts that are known statically. For instance, even though the invariants describing the behavior of two functions f1 and f2 may be unknown, we may know that any valid input for f1 is also valid for f2. This fact can be incorporated in the inference process to eliminate inconsistent invariants. More generally, the work explores techniques for expressing, discovering, and employing such consistency constraints to improve the quality of produced invariants, from type information and other sources including static analysis and user-supplied annotation. The work will impact many aspects of software engineering, including scientific and industrial uses. Concrete benefits will be in the form of publications, usable software (released under an academic open-source license), software prototypes, and educational activities and resources (enhancement of a textbook and current courses, internships for high school students).