Marius Bozga and Radu Iosif
Quantitative Verification of Programs with Lists (2005)
Quantitative Verification of Programs with Lists (2005)
TR-2005-2.ps
Keywords: Hoare logic, first-order arithmetic, quantitative shape analysis, counter automata.
Abstract: In this paper we study imperative programs that handle list objects, performing unrestricted selector updating operations. For this class of programs, we address the problem of {em quantitative verification}, by reasoning about arithmetic relations between the lengths of certain lists. We first show undecidability of the general problem, by reduction from the reachability problem for two-counter machines. Second, we introduce a decidable property specification logic and we study the complexity of the decision problem. Finally, we propose a semi-algorithmic method for the verification of Hoare-Floyd style properties of programs with lists. Using this method, we can reduce the invariant computation problem for a program with lists to an acceleration problem for integer counter automata.
