2008 23rd IEEE/ACM International Conference on Automated Software Engineering (2008)
Sept. 15, 2008 to Sept. 19, 2008
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ASE.2008.55
T.E. Hart , Dept. of Comput. Sci., Univ. of Toronto, Toronto, ON
K. Ku , Dept. of Comput. Sci., Univ. of Toronto, Toronto, ON
Existing software model checkers based on predicate abstraction and refinement typically perform poorly at verifying the absence of buffer overflows, with analyses depending on the sizes of the arrays checked. We observe that many of these analyses can be made efficient by providing proof templates for common array traversal idioms idioms, which guide the model checker towards proofs that are independent of array size. We have integrated this technique into our software model checker, PtYasm, and have evaluated our approach on a set of testcases derived from the Verisec suite, demonstrating that our technique enables verification of the safety of array accesses independently of array size.
safety verification, counterexample-guided abstraction refinement, proof templates, software model checkers, predicate abstraction, buffer overflows verification, array traversal idioms, PtYasm, Verisec suite
D. Lie, M. Chechik, K. Ku, T. Hart and A. Gurfinkel, "Augmenting Counterexample-Guided Abstraction Refinement with Proof Templates," 2008 23rd IEEE/ACM International Conference on Automated Software Engineering(ASE), L'Aquila, 2008, pp. 387-390.