Select a calendar:
Filter September Events by Event Type:
SUNMONTUEWEDTHUFRISAT
Events for September 08, 2016
-
Invariant Inference for Program Specification and Verification
Thu, Sep 08, 2016 @ 04:00 PM - 05:00 PM
Ming Hsieh Department of Electrical and Computer Engineering
Conferences, Lectures, & Seminars
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
-
EE 598 Computer Engineering Seminar
Thu, Sep 08, 2016 @ 04:00 PM - 05:00 PM
Ming Hsieh Department of Electrical and Computer Engineering
Conferences, Lectures, & Seminars
Speaker: Todd Millstein, Professor, University of California, Los Angeles
Talk 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.
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
Location: Olin Hall of Engineering (OHE) - OHE 100D
Audiences: Everyone Is Invited
Contact: Estela Lopez
