Sciweavers

Share
SAS
2010
Springer

Statically Inferring Complex Heap, Array, and Numeric Invariants

10 years 2 months ago
Statically Inferring Complex Heap, Array, and Numeric Invariants
We describe Deskcheck, a parametric static analyzer that is able to establish properties of programs that manipulate dynamically allocated memory, arrays, and integers. Deskcheck can verify quantified ts over mixed abstract domains, e.g., heap and numeric domains. These domains need only minor extensions to work with our domain combination framework. The technique used for managing the communication between domains is reminiscent of the Nelson-Oppen technique for combining decision procedures, in that the two domains share a common predicate language to exchange shared facts. However, whereas the Nelson-Oppen technique is limited to a common predicate language of shared equalities, the technique described in this paper uses a common predicate language in which shared facts can be quantified predicates expressed in first-order logic with transitive closure. We explain how we used Deskcheck to establish memory safety of the thttpd web server’s cache data structure, which uses linked...
Bill McCloskey, Thomas W. Reps, Mooly Sagiv
Added 30 Jan 2011
Updated 30 Jan 2011
Type Journal
Year 2010
Where SAS
Authors Bill McCloskey, Thomas W. Reps, Mooly Sagiv
Comments (0)
books