Calysto: Scalable and Precise Extended Static Checking
[PDF] [PS] [PS.BZ2] [VIEW]
Bibtex:
@inproceedings{bh08calysto,
author = {Domagoj Babi\'c and Alan J. Hu},
title = {{Calysto: Scalable and Precise Extended Static Checking}},
booktitle = {ICSE'08: Proceedings of the 30th International
Conference on Software Engineering},
month = {May},
year = {2008},
pages = {211--220},
publisher = {ACM},
address = {New York, NY, USA},
location = {Leipzig, Germany},
doi = {http://doi.acm.org/10.1145/1368088.1368118},
isbn = {978-1-60558-079-1},
}
Abstract:
Automatically detecting bugs in programs has been a long-held
goal in software engineering. Many techniques exist, trading-off
varying levels of automation, thoroughness of coverage of program
behavior, precision of analysis, and scalability to large code bases.
This paper presents the CALYSTO static checker, which achieves an
unprecedented combination of precision and scalability in a completely
automatic extended static checker. CALYSTO is interprocedurally
path-sensitive, fully context-sensitive, and bit-accurate in
modeling data operations — comparable coverage and precision
to very expensive formal analyses — yet scales comparably to the
leading, less precise, static-analysis-based tool for similar properties.
Using CALYSTO, we have discovered dozens of bugs, completely
automatically, in hundreds of thousands of lines of production,
open-source applications, with a very low rate of false error
reports. This paper presents the design decisions, algorithms, and
optimizations behind CALYSTO’s performance.