×

Verification of multi-linked heaps. (English) Zbl 1246.68093

Summary: We define the class of single-parent heap systems, which rely on a singly-linked heap in order to model destructive updates on tree structures. This encoding has the advantage of relying on a relatively simple theory of linked lists in order to support abstraction computation. To facilitate the application of this encoding, we provide a program transformation that, given a program operating on a multi-linked heap without sharing, transforms it into one over a single-parent heap. It is then possible to apply shape analysis by predicate and ranking abstraction. The technique has been successfully applied on examples with lists (reversal and bubble sort) and trees with of fixed arity (balancing of, and insertion into, a binary sort tree).

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

JTLV
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Arons, Tamarah; Pnueli, Amir; Ruah, Sitvanit; Xu, Jiazhao; Zuck, Lenore D., Parameterized verification with automatically computed inductive assertions, (Proc. 13rd Intl. Conference on Computer Aided Verification. Proc. 13rd Intl. Conference on Computer Aided Verification, Lecture Notes in Comput. Sci., vol. 2102 (2001)), 221-234 · Zbl 0991.68541
[2] Ittai Balaban, Shape analysis by augmentation, abstraction, and transformation, PhD thesis, New York University, New York, May 2007.; Ittai Balaban, Shape analysis by augmentation, abstraction, and transformation, PhD thesis, New York University, New York, May 2007.
[3] Balaban, Ittai; Pnueli, Amir; Zuck, Lenore D., Shape analysis by predicate abstraction, (Cousot, Radhia, Proc. of the 6th Int. Conference on Verification, Model Checking, and Abstract Interpretation. Proc. of the 6th Int. Conference on Verification, Model Checking, and Abstract Interpretation, Lecture Notes in Comput. Sci., vol. 3385 (2005), Springer), 164-180 · Zbl 1111.68396
[4] Balaban, Ittai; Pnueli, Amir; Zuck, Lenore D., Modular ranking abstraction, Internat. J. Found. Comput. Sci., 18, 1, 5-44 (2007) · Zbl 1109.68062
[5] Ittai Balaban, Amir Pnueli, Lenore D. Zuck, Shape analysis of single-parent heaps, in: Proc. of the 8th Int. Conference on Verification, Model Checking, and Abstract Interpretation, 2007, pp. 91-105.; Ittai Balaban, Amir Pnueli, Lenore D. Zuck, Shape analysis of single-parent heaps, in: Proc. of the 8th Int. Conference on Verification, Model Checking, and Abstract Interpretation, 2007, pp. 91-105. · Zbl 1132.68346
[6] Thomas Ball, Andreas Podelski, Sriram K. Rajamani, Relative completeness of abstraction refinement for software model checking, in: Tools and Algorithms for Construction and Analysis of Systems, 2002, pp. 158-172.; Thomas Ball, Andreas Podelski, Sriram K. Rajamani, Relative completeness of abstraction refinement for software model checking, in: Tools and Algorithms for Construction and Analysis of Systems, 2002, pp. 158-172. · Zbl 1043.68523
[7] Thomas Ball, Sriram K. Rajamani, Automatically validating temporal safety properties of interfaces, in: Lecture Notes in Comput. Sci., vol. 2057, 2001, pp. 103-122.; Thomas Ball, Sriram K. Rajamani, Automatically validating temporal safety properties of interfaces, in: Lecture Notes in Comput. Sci., vol. 2057, 2001, pp. 103-122. · Zbl 0985.68641
[8] Michael Benedikt, Thomas W. Reps, Shmuel Sagiv, A decidable logic for describing linked data structures, in: ESOP, 1999, pp. 2-19.; Michael Benedikt, Thomas W. Reps, Shmuel Sagiv, A decidable logic for describing linked data structures, in: ESOP, 1999, pp. 2-19.
[9] Josh Berdine, Byron Cook, Dino Distefano, Peter W. OʼHearn, Automatic termination proofs for programs with shape-shifting heaps, in: CAV, 2006, pp. 386-400.; Josh Berdine, Byron Cook, Dino Distefano, Peter W. OʼHearn, Automatic termination proofs for programs with shape-shifting heaps, in: CAV, 2006, pp. 386-400. · Zbl 1188.68109
[10] Jesse D. Bingham, Zvonimir Rakamaric, A logic and decision procedure for predicate abstraction of heap-manipulating programs, in: VMCAI, 2006, pp. 207-221.; Jesse D. Bingham, Zvonimir Rakamaric, A logic and decision procedure for predicate abstraction of heap-manipulating programs, in: VMCAI, 2006, pp. 207-221. · Zbl 1176.68113
[11] Börger, Egon; Grädel, Erich; Gurevich, Yuri, The Classical Decision Problem, Perspect. Math. Logic (1997), Springer-Verlag, second printing, Universitext, 2001 · Zbl 0865.03004
[12] Ahmed Bouajjani, Marius Bozga, Peter Habermehl, Radu Iosif, Pierre Moro, Tomás Vojnar, Programs with lists are counter automata, in: CAV, 2006, pp. 517-531.; Ahmed Bouajjani, Marius Bozga, Peter Habermehl, Radu Iosif, Pierre Moro, Tomás Vojnar, Programs with lists are counter automata, in: CAV, 2006, pp. 517-531. · Zbl 1188.68181
[13] Bouajjani, Ahmed; Dragoi, Cezara; Enea, Constantin; Sighireanu, Mihaela, A logic-based framework for reasoning about composite data structures, (Bravetti, Mario; Zavattaro, Gianluigi, CONCUR. CONCUR, Lecture Notes in Comput. Sci., vol. 5710 (2009), Springer), 178-195 · Zbl 1254.68146
[14] Clarke, Edmund M.; Emerson, E. Allen, Design and synthesis of synchronization skeletons using branching time temporal logic, (Proc. IBM Workshop on Logics of Programs. Proc. IBM Workshop on Logics of Programs, Lecture Notes in Comput. Sci., vol. 131 (1981), Springer-Verlag), 52-71 · Zbl 0546.68014
[15] Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith, Counterexample-guided abstraction refinement, in: Computer Aided Verification, 2000, pp. 154-169.; Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith, Counterexample-guided abstraction refinement, in: Computer Aided Verification, 2000, pp. 154-169. · Zbl 0974.68517
[16] Emerson, E. Allen; Clarke, Edmund M., Characterizing correctness properties of parallel programs using fixpoints, (Lecture Notes in Comput. Sci., vol. 85 (1980), Springer-Verlag), 169-181 · Zbl 0456.68016
[17] Erich Grädel, Martin Otto, Eric Rosen, Undecidability results on two-variable logics, in: STACS, 1997, pp. 249-260.; Erich Grädel, Martin Otto, Eric Rosen, Undecidability results on two-variable logics, in: STACS, 1997, pp. 249-260.
[18] Gulwani, Sumit; Lev-Ami, Tal; Sagiv, Mooly, A combination framework for tracking partition sizes, (Shao, Zhong; Pierce, Benjamin C., POPL (2009), ACM), 239-251 · Zbl 1315.68094
[19] Neil Immerman, Alexander M. Rabinovich, Thomas W. Reps, Shmuel Sagiv, Greta Yorsh, The boundary between decidability and undecidability for transitive-closure logics, in: CSL, 2004, pp. 160-174.; Neil Immerman, Alexander M. Rabinovich, Thomas W. Reps, Shmuel Sagiv, Greta Yorsh, The boundary between decidability and undecidability for transitive-closure logics, in: CSL, 2004, pp. 160-174. · Zbl 1095.03008
[20] Immerman, Neil; Rabinovich, Alexander M.; Reps, Thomas W.; Sagiv, Shmuel; Yorsh, Greta, Verification via structure simulation, (Proc. 16th Intl. Conference on Computer Aided Verification. Proc. 16th Intl. Conference on Computer Aided Verification, Lecture Notes in Comput. Sci. (2004), Springer-Verlag), 281-294 · Zbl 1103.68623
[21] Jones, Neil D.; Muchnick, Steven S., Flow analysis and optimization of Lisp-like structures, (Muchnick, Steven S.; Jones, Neil D., Program Flow Analysis: Theory and Applications, Chapter 4 (1981), Prentice Hall: Prentice Hall Englewood Cliffs, NJ), 102-131
[22] Kesten, Yonit; Pnueli, Amir, Verification by augmented finitary abstraction, Inform. and Comput., 163, 1, 203-243 (2000) · Zbl 1003.68069
[23] Klarlund, Nils; Schwartzbach, Michael I., Graph types, (Proc. 20th ACM Symp. Princ. of Prog. Lang. (1993), ACM Press: ACM Press New York, NY, USA), 196-205
[24] Manevich, Roman; Yahav, Eran; Ramalingam, Ganesan; Sagiv, Shmuel, Predicate abstraction and canonical abstraction for singly-linked lists, (Cousot, Radhia, Proc. of the 6th Int. Conference on Verification, Model Checking, and Abstract Interpretation. Proc. of the 6th Int. Conference on Verification, Model Checking, and Abstract Interpretation, Lecture Notes in Comput. Sci., vol. 3385 (2005), Springer), 181-198 · Zbl 1111.68398
[25] Anders Møller, Michael I. Schwartzbach, The pointer assertion logic engine, in: Programming Language Design and Implementation, 2001.; Anders Møller, Michael I. Schwartzbach, The pointer assertion logic engine, in: Programming Language Design and Implementation, 2001.
[26] Pnueli, Amir; Saʼar, Yaniv; Zuck, Lenore D., JTLV: A framework for developing verification algorithms, (Proc. 22nd Intl. Conference on Computer Aided Verification. Proc. 22nd Intl. Conference on Computer Aided Verification, Lecture Notes in Comput. Sci., vol. 6174 (2010), Springer), 171-174
[27] Andreas Podelski, Private communication, January 2010.; Andreas Podelski, Private communication, January 2010.
[28] John C. Reynolds, Separation logic: A logic for shared mutable data structures, in: LICS, 2002, pp. 55-74.; John C. Reynolds, Separation logic: A logic for shared mutable data structures, in: LICS, 2002, pp. 55-74.
[29] Graf, Susanne; Saïdi, Hassen, Construction of abstract state graphs with PVS, (Grumberg, O., Proc. 9th International Conference on Computer Aided Verification (CAVʼ97), vol. 1254 (1997), Springer-Verlag), 72-83
[30] Thomas Wies, Viktor Kuncak, Patrick Lam, Andreas Podelski, Martin C. Rinard, Field constraint analysis, in: Proc. of the 7th Int. Conference on Verification, Model Checking, and Abstract Interpretation, 2006.; Thomas Wies, Viktor Kuncak, Patrick Lam, Andreas Podelski, Martin C. Rinard, Field constraint analysis, in: Proc. of the 7th Int. Conference on Verification, Model Checking, and Abstract Interpretation, 2006. · Zbl 1176.68130
[31] Greta Yorsh, Alexander M. Rabinovich, Mooly Sagiv, Antoine Meyer, Ahmed Bouajjani, A logic of reachable patterns in linked data-structures, in: FoSSaCS, 2006, pp. 94-110.; Greta Yorsh, Alexander M. Rabinovich, Mooly Sagiv, Antoine Meyer, Ahmed Bouajjani, A logic of reachable patterns in linked data-structures, in: FoSSaCS, 2006, pp. 94-110. · Zbl 1180.68131
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.