Summary Based Static Analysis for Practical Search for Defects in C Programs and Libraries

This paper considers an algorithm for scalable automatic static analysis to detect defects in programs written in C. We propose a criterion for emitting warnings based on reach ability of function statements. Main advantages of the proposed approach are scalability, high true positive rate and ability to perform library analysis.