VINTA: Combining Model Checking and Abstract Interpretation

The Faculty of Informatics is pleased to announce a seminar given by Arie Gurfinkel

DATE: Thursday, January 24th 2013
PLACE: USI Università della Svizzera italiana, room SI-006, Informatics building (Via G. Buffi 13)
TIME: 15.30

ABSTRACT:
Abstract interpretation (AI) is one of the most scalable automated program verification techniques.  The scalability is achieved through aggressive abstraction in basic analysis steps (i.e., joins and widening). This leads to loss of precision. As such, AI is plagued by false alarms. In this talk, I will present VINTA, an algorithm that enriches AI with Abstraction Refinement techniques from Model Checking to alleviate the false alarms. VINTA is an iterative algorithm that uses Craig interpolants to refine and guide AI away from false alarms. VINTA is based on a novel refinement strategy that capitalizes on recent advances in SMT and interpolation-based Model Checking. On one hand, it can find concrete counterexamples to justify alarms produced by AI. On the other, it can strengthen invariants to exclude alarms that cannot be justified. The refinement process continues until either a safe inductive invariant is computed, a counterexample is found, or resources are exhausted. This strategy allows VINTA to recover precision lost in many AI steps. VINTA has been implemented as part of the UFO verification framework. It is a big contributor to the success of UFO in the 2nd International Software Verification Competition.

BIO:
Arie Gurfinkel received a Ph.D. in Computer Science from the Computer  Science Department of University of Toronto in 2007. He is currently a Senior Researcher at the Carnegie Mellon Software Engineering  Institute and a Research Scientist at the School of Computer Science  at Carnegie Mellon University. His research interests lie in the intersection of formal methods and software engineering, with an emphasis on automated reasoning about software systems. He is a lead developer for a number of automated verification tools including a multi-valued model-checker XChek, a software model-checker Yasm. His most recent tool, UFO, developed in collaboration with University of Toronto has won 4 gold medals at the 2nd International Software Verification Competition (SV-COMP'13).

HOST: Prof. Natasha Sharygina