Abstract:

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 paper, we present 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 easily scales to over 200,000 lines of real C/C++ code.

Published:

"Structural Abstraction of Software Verification Conditions"
Domagoj Babic and Alan J. Hu.
Proc. of the 19th International Conference on Computer Aided Verification (CAV'07) , Berlin, Germany, July 3-7, 2007.

Download:

Paper:

• "Structural Abstraction of Software Verification Conditions" (PDF)

BibTeX Entry:

@inproceedings{bh07structural,
  author = {Domagoj Babi\'c and Alan J. Hu},
  title = {{Structural Abstraction of Software Verification Conditions}},
  booktitle = {Proceedings of the 19th Int. Conf. on Computer Aided Verification
               (CAV'07), Berlin, Germany}
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  year = {2007},
  month = {July}
}