Structural Abstraction of Software Verification Conditions

September 17, 2007
Domagoj Babic | University of British Columbia

Precise software analysis and verification require tracking the exact path along which a statement is executed (path-sensitivity), the different contexts from which a function is called (context-sensitivity), and the bit-accurate operations performed. Previously, verification with such precision has been considered too inefficient to scale to large software.
In this talk, Domagoj presents a novel approach to solving such verification conditions, based on an automatic abstraction-checking-refinement framework that exploits natural abstraction boundaries present in software.
Experimental results show that our approach scales to over 200,000 lines of real C code.

Speaker Details

Domagoj Babic is a Ph.D. candidate at the University of British Columbia. His research interests include software verification and analysis, as well as automated theorem proving and SAT solving.

Domagoj holds a M.Sc. degree in computer science and a Dipl.Ing.
degree in industrial electronics from the Faculty of Electrical Engineering and Computing at Zagreb University. He is a Microsoft fellow (2005-2007).

For more information, see http://www.domagoj.info/