Abstract
We describe a program verification methodology for specifying global shape properties of data structures by means of axioms involving predicates on scalar fields, pointer equalities, and pointer disequalities, in the neighborhood of a memory cell. We show that such local invariants are both natural and sufficient for describing a large class of data structures. We describe a complete decision procedure for axioms without disequalities, and practical heuristics for the full language. The procedure has the key advantage that it can be extended easily with reasoning for any decidable theory of scalar fields.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Cantone, D., Zarba, C.G.: A new fast decision procedure for an unquantified fragment of set theory. First-Order Theorem Proving, 97–105 (1998)
Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A theorem prover for program checking. Technical Report HPL-2003-148, HP Labs (July 2003)
Detlefs, D.L., Leino, K.R.M., Nelson, G., Saxe, J.B.: Extended static checking. Technical Report SRC-159, COMPAQ SRC, Palo Alto, USA (December 1998)
Fradet, P., Métayer, D.L.: Shape types. In: POPL, pp. 27–39 (1997)
Hackett, B., Rugina, R.: Region-based shape analysis with tracked locations. In: POPL, pp. 310–323 (2005)
Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., Yorsh, G.: The boundary between decidability and undecidability for transitive-closure logics. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 160–174. Springer, Heidelberg (2004)
Klarlund, N., Schwartzbach, M.: Graph types. In: POPL, pp. 196–205 (1993)
Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebra. In: Leech, J. (ed.) Computational Problems in Abstract Algebras, pp. 263–297. Pergamon Press, Oxford (1970)
Kuncak, V., Lam, P., Rinard, M.: Role analysis. In: POPL, pp. 17–32 (2002)
Kuncak, V., Rinard, M.: Existential heap abstraction entailment is undecidable. In: SAS, pp. 418–438 (2003)
Leino, K.R.M., Müller, P.: Object invariants in dynamic contexts. In: European Conference on Object-Oriented Programming, ECOOP (2004)
Lev-Ami, T., Sagiv, S.: TVLA: A system for implementing static analyses. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, pp. 280–301. Springer, Heidelberg (2000)
Möller, A., Schwartzbach, M.: The pointer assertion logic engine. In: PLDI, pp. 221–231 (2001)
Nelson, G.: Techniques for program verification. Technical Report CSL-81-10, Xerox Palo Alto Research Center (1981)
Nelson, G.: Verifying reachability invariants of linked structures. In: POPL, pp. 38–47 (1983)
Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. JACM 27(2), 356–364 (1980)
Oppen, D.C.: Reasoning about recursively defined data structures. JACM 27(3), 403–411 (1980)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. Logic in Computer Science, pp. 55–74 (2002)
Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. TOPLAS 24(3), 217–298 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
McPeak, S., Necula, G.C. (2005). Data Structure Specifications via Local Equality Axioms. In: Etessami, K., Rajamani, S.K. (eds) Computer Aided Verification. CAV 2005. Lecture Notes in Computer Science, vol 3576. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11513988_47
Download citation
DOI: https://doi.org/10.1007/11513988_47
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-27231-1
Online ISBN: 978-3-540-31686-2
eBook Packages: Computer ScienceComputer Science (R0)