From Under-approximations to Over-approximations and Back
Staff - Faculty of Informatics
Start date: 29 May 2012
End date: 30 May 2012
The Faculty of Informatics is pleased to announce a seminar given by Arie Gurfinkel
DATE: Tuesday, May 29th, 2012
PLACE: USI Università della Svizzera italiana, room SI-006, Informatics building (Via G. Buffi 13)
TIME: 14.30
ABSTRACT:
Current approaches to software model checking can be divided into over-approximation-driven (OD) and under-approximation-driven (UD). OD approaches maintain an abstraction of the transition relation of a program and use abstract reachability to build an inductive invariant (or find a counterexample). At the other extreme, DU approaches attempt to construct inductive invariants by generalizing from finite paths through the control-flow graph of the program.
In this talk, I will present UFO, a framework that unifies OD and UD approaches in order to leverage both of their advantages. UFO is parameterized by the degree to which over- and under-approximations drive the analysis. At one extreme, UFO is a novel interpolation-based (UD) algorithm that generates interpolants to label (i.e., refine) multiple program paths using only a single SMT solver query. At the other extreme, UFO uses an abstract domain to drive the analysis, while using interpolants to strengthen the abstraction.
UFO has been implemented in the LLVM compile infrustructure. Our experimental results demonstrate the utility of our algorithm and the benefits of combining UD and OD approaches when applied to benchmakrs from the Competition on Software Verification.
This is joint work with Aws Albarghouthi and Marsha Chechik from University of Toronto.
BIO:
Arie Gurfinkel received a Ph.D., a M.Sc., and a B.Sc. in Computer Science from Computer Science Department of University of Toronto in 2007, 2003, and 2000, respectively. He is currently a Senior Member of Technical Staff at the Software Engineering Institute at Carnegie Mellon University. His research interests lie in the intersection of formal methods and software engineering, with an emphasis on automated techniques for program verification. He was a lead developer for a number of automated verification tools including a multi-valued model-checker XChek, a software model-checker Yasm, and a program analysis framework UFO. He has over 50 publications in peer reviewed journals and conferences.
HOST: Prof. Natasha Sharygina
