Date	September 8, 2016
Speaker	Todd Millstein University of California, Los Angeles
Title	Invariant Inference for Program Specification and Verification
Abstract	Why isn't software verification technology in common use today? One reason is that, despite decades of foundational and practical advances, verification is still too costly in terms of human time and effort. I'll describe my recent research with colleagues to address two of the most onerous parts of the software verification process: creating a high-quality specification, and identifying the inductive program invariants that form the key lemmas in a proof of software correctness. Our research supports both tasks through a new form of automatic invariant inference that is both more expressive and less burdensome than prior techniques. We extend the data-driven approach to invariant inference, whereby program invariants are learned from a set of test executions. This approach is appealingly general, as it naturally handles arbitrarily complex code and specifications. However, prior data-driven techniques have required the user to provide a fixed set of "features" as input, which are atomic predicates that define the search space of possible invariants. If these features are insufficient, invariant inference will either fail or produce an incorrect result. In contrast, we introduce a technique for on-demand feature learning, which automatically expands the search space of candidate invariants in a targeted manner on demand. Our approach eliminates the problem of feature selection and guarantees that inferred invariants are consistent with the given tests. We have used our technique both to infer rich specifications for black-box code and to infer provably correct loop invariants as part of an automatic program verifier.
Bio	Todd Millstein is a Professor in the Computer Science Department at the University of California, Los Angeles. His research interests are broadly in programming languages and software verification. Todd received his Ph.D. and M.S. from the University of Washington and his A.B. from Brown University, all in Computer Science. Todd received an NSF CAREER award in 2006, an IBM Faculty Award in 2008, an ACM SIGPLAN Most Influential PLDI Paper Award in 2011, an IEEE Micro Top Picks selection in 2012, the Northrop Grumman Excellence in Teaching Award from UCLA Engineering in 2016, and a Microsoft Research Outstanding Collaborator Award in 2016.
Resources