Abstract
The ability to statically detect violations of assertions can add great value to developers. However, in spite of decades of progress in program verification, static assertion checking is far from being cost-effective for production software. The two main obstacles to finding high-quality defects are (a) false alarms due to under-constrained environment, and (b) finding violations to deeply nested procedures.
In this talk, we will describe our experience with the angelic verification (AV) tool for statically finding assertion violations in real-world software. The basic idea of AV is to pair an interprocedural assertion verifier with a framework for automatic inference of likely specifications on unknown values from the environment. We will summarize the approach, and will focus on design choices required to find high-quality violations of memory-safety violations with low false alarms. We discuss some results on Microsoft codebases and open source software, and challenges ahead.
Citation
Shaobo He,
Shuvendu Lahiri,
Akash Lal,
Zvonimir Rakamaric
Static Assertion Checking of Production Software with Angelic Verification
8th Workshop on Tools for Automatic Program Analysis (TAPAS), 2017.
BibTeX
@inproceedings{2017_tapas_hllr,
title = {Static Assertion Checking of Production Software with Angelic Verification},
author = {Shaobo He and Shuvendu Lahiri and Akash Lal and Zvonimir Rakamaric},
booktitle = {8th Workshop on Tools for Automatic Program Analysis (TAPAS)},
note = {Extended abstract},
year = {2017}
}