Bill McCloskey and Mooly Sagiv

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2009-106

July 30, 2009

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2009/EECS-2009-106.pdf

We develop general algorithms for reasoning about numerical properties of programs manipulating the heap via pointers. We automatically infer quantified invariants regarding unbounded sets of memory locations and unbounded numeric values. As an example, we can infer that for every node in a data structure, the node's length field is less than its capacity field. We can also infer per-node statements about cardinality, such as that each node's count field is equal to the number of elements reachable from it. This additional power allows us to prove properties about reference counted data structures and B-trees that were previously unattainable. Besides the ability to verify more programs, we believe that our work sheds new light on the interaction between heap and numerical reasoning.

Our algorithms are parametric in the heap and the numeric abstractions. They permit heap and numerical abstractions to be combined into a single abstraction while maintaining correlations between these abstractions. In certain combinations not involving cardinality, we prove that our combination technique is complete, which is surprising in the presence of quantification.

---

BibTeX citation:

@techreport{McCloskey:EECS-2009-106,
    Author= {McCloskey, Bill and Sagiv, Mooly},
    Title= {Combining Quantified Domains},
    Year= {2009},
    Month= {Jul},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2009/EECS-2009-106.html},
    Number= {UCB/EECS-2009-106},
    Abstract= {We develop general algorithms for reasoning about numerical properties of programs manipulating the heap via pointers.  We automatically infer quantified invariants regarding unbounded sets of memory locations and unbounded numeric values.  As an example, we can infer that for every node in a data structure, the node's length field is less than its capacity field. We can also infer per-node statements about cardinality, such as that each node's count field is equal to the number of elements reachable from it.  This additional power allows us to prove properties about reference counted data structures and B-trees that were previously unattainable.  Besides the ability to verify more programs, we believe that our work sheds new light on the interaction between heap and numerical reasoning.

Our algorithms are parametric in the heap and the numeric
abstractions. They permit heap and numerical abstractions to be combined into a single abstraction while maintaining correlations between these abstractions.  In certain combinations not involving cardinality, we prove that our combination technique is complete, which is surprising in the presence of quantification.},
}

EndNote citation:

%0 Report
%A McCloskey, Bill 
%A Sagiv, Mooly 
%T Combining Quantified Domains
%I EECS Department, University of California, Berkeley
%D 2009
%8 July 30
%@ UCB/EECS-2009-106
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2009/EECS-2009-106.html
%F McCloskey:EECS-2009-106