Combining Predicate and Numeric Abstraction for Software Model Checking (Extended Abstract)

Arie Gurfinkel, Sagar Chaki, Proceedings of the 6th NASA Langley Formal Methods Workshop (LFM), 2008.

Abstract: This paper presents techniques for tight coupling between predicate abstraction based software model checking and numeric domain based abstract interpretation for more efficient software analysis. We describe four different data structures to achieve such tight coupling, and compare and contrast between them on the basis of experimental measurements.