Events Calendar

Invariant Inference for Program Specification and Verification

Speaker: Todd Millstein, University of California, Los Angeles

Talk Title: Invariant Inference for Program Specification and Verification

Series: EE 598 Computer Engineering Seminar Series

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.

Joint work with Saswat Padhi (UCLA) and Rahul Sharma (Stanford).




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


Host: Xuehai Qian, x04459, xuehai.qian@usc.edu

Location: Olin Hall of Engineering (OHE) - 100D

Audiences: Everyone Is Invited

Contact: Gerrielyn Ramos