NASA Logo, National Aeronautics and Space Administration
Intelligent Systems Division Banner


aiken image
Alex Aiken
Stanford University
Using Learning Techniques in Invariant Inference

Arguably the hardest problem in automatic program veri cation is designing appropriate techniques for discovering loop invariants (or, more generally, recursive procedures). Certainly, if invariants are known, the rest of the veri cation problem becomes easier. This talk presents a family of invariant inference techniques based on using test cases to generate an under-approximation of program behavior and then using machine learning algorithms to generalize the under-approximation to an invariant. These techniques are simpler, much more efficient, and appear to be more robust than previous approaches to the problem. If time permits, some open problems will also be discussed.

First Gov logo
NASA Logo - nasa.gov