VINTA: Combining Model Checking and Abstract Interpretation

June 4, 2013
Arie Gurfinkel | Carnegie Mellon University

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., post, join 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 Software 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. It 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

Speaker Details

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 between Software Engineering Institute and University of Toronto has won 4 gold medals at the 2nd International Software Verification Competition (SV-COMP’13).