Verifying properties of well-founded linked lists. (English) Zbl 1369.68143
Proceedings of the 33rd ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’06, Charleston, SC, USA, January 11–13, 2006. New York, NY: Association for Computing Machinery (ACM) (ISBN 1-59593-027-2). 115-126 (2006).
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68P05 | Data structures |
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
Keywords:
automated theorem proving; decision procedure; first-order axiomatization; heap abstraction; well-founded linked listsReferences:
| [1] | T. Andrews, S. Qadeer, S. K. Rajamani, J. Rehof, and Y. Xie. Zing: Exploiting program structure for model checking concurrent software. In CONCUR 04: 15th International Conference on Concurrency Theory, volume 3170 of LNCS, pages 1-15. Springer-Verlag, 2004.]] · Zbl 1099.68583 |
| [2] | I. Balaban, A. Pnueli, and L. D. Zuck. Shape analysis by predicate abstraction. In VMCAI 05: Verification, Model checking, and Abstract Interpretation, volume 3385 of LNCS, pages 164-180. Springer-Verlag, 2005.]] 10.1007/978-3-540-30579-8_12 · Zbl 1111.68396 |
| [3] | T. Ball, R. Majumdar, T. Millstein, and S. K. Rajamani. Automatic predicate abstraction of C programs. In PLDI 01: Programming Language Design and Implementation, pages 203-213, 2001.]] 10.1145/378795.378846 |
| [4] | C. Barrett and S. Berezin. CVC Lite: A new implementation of the cooperating validity checker. In Computer Aided Verification (CAV’04), volume 3114 of LNCS, pages 515-518. Springer-Verlag, 2004.]] · Zbl 1103.68605 |
| [5] | M. Benedikt, Thomas W. Reps, and S. Sagiv. A decidable logic for describing linked data structures. In ESOP 99: European Symposium on Programming, volume 1576 of LNCS, pages 2-19. Springer-Verlag, 1999.]] |
| [6] | J. Berdine, C. Calcagno, and P. W. O’Hearn. A decidable fragment of separation logic. In FSTTCS 04: Foundations of Software Technology and Theoretical Computer Science, volume 3328 of LNCS, pages 97-109. Springer-Verlag, 2004.]] · Zbl 1117.03337 |
| [7] | R. E. Bryant, S. K. Lahiri, and S. A. Seshia. Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In Computer-Aided Verification (CAV’02), volume 2404 of LNCS, pages 78-92, July 2002.]] · Zbl 1010.68522 |
| [8] | D. Dams and K. S. Namjoshi. Shape analysis through predicate abstraction and model checking. In VMCAI 03: Verification, Model checking, and Abstract Interpretation, volume 2575 of LNCS, pages 310-324. Springer-Verlag, 2003.]] · Zbl 1022.68578 |
| [9] | D. L. Detlefs, G. Nelson, and J. B. Saxe. Simplify: A theorem prover for program checking. Technical report, HPL-2003-148, 2003.]] |
| [10] | E.W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.]] · Zbl 0368.68005 |
| [11] | G. Dong and J. Su. Incremental and decremental evaluation of transitive closure by first-order queries. Information and Computation, 120(1):101-106, 1995.]] 10.1006/inco.1995.1102 · Zbl 0835.68031 |
| [12] | C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata. Extended static checking for Java. In PLDI 02: Programming Language Design and Implementation, pages 234-245. ACM Press, 2002.]] 10.1145/512529.512558 |
| [13] | C. Flanagan and S. Qadeer. Predicate abstraction for software verification. In POPL 02: Principles of Programming Languages, pages 191-202. ACM Press, 2002.]] 10.1145/503272.503291 · Zbl 1323.68371 |
| [14] | R. Ghiya and L. J. Hendren. Is it a tree, a DAG, or a cyclic graph? A shape analysis for heap-directed pointers in C. In POPL 96: Principles of Programming Languages, pages 1-15. ACM Press, 1996.]] 10.1145/237721.237724 |
| [15] | S. Graf and H. Saïdi. Construction of abstract state graphs with PVS. In Computer-Aided Verification (CAV ’97), volume 1254 of LNCS, pages 72-83. Springer-Verlag, June 1997.]] |
| [16] | B. Hackett and R. Rugina. Region-based shape analysis with tracked locations. In POPL 05: Principles of Programming Languages, pages 310-323. ACM Press, 2005.]] 10.1145/1040305.1040331 · Zbl 1369.68140 |
| [17] | T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In POPL 02: Principles of Programming Languages, pages 58-70. ACM Press, 2002.]] 10.1145/503272.503279 · Zbl 1323.68374 |
| [18] | N. Immerman, A. M. Rabinovich, T. W. Reps, S. Sagiv, and G. Yorsh. The boundary between decidability and undecidability for transitive-closure logics. In CSL 04: Computer Science Logic, volume 3210 of LNCS, pages 160-174. Springer-Verlag, 2004.]] · Zbl 1095.03008 |
| [19] | S. S. Ishtiaq and P. W. O’Hearn. BI as an assertion language for mutable data structures. In POPL 01: Principles of Programming Languages, pages 14-26. ACM Press, 2001.]] 10.1145/360204.375719 · Zbl 1323.68077 |
| [20] | N. Klarlund and M. I. Schwartzbach. Graph types. In POPL 93: Principles of Programming Languages, pages 196-205. ACM Press, 1993.]] 10.1145/158511.158628 |
| [21] | S. K. Lahiri and R. E. Bryant. Constructing quantified invariants via predicate abstraction. In VMCAI 04: Verification, Model Checking and Abstract Interpretation, volume 2937 of LNCS, pages 267-281. Springer-Verlag, 2004.]] · Zbl 1202.68251 |
| [22] | S. K. Lahiri and R. E. Bryant. Indexed predicate discovery for unbounded system verification. In Computer Aided Verification (CAV’04), volume 3114 of LNCS, pages 135-147. Springer-Verlag, 2004.]] · Zbl 1103.68627 |
| [23] | S. K. Lahiri and S. Qadeer. Verifying properties of well-founded linked lists. Technical Report MSR-TR-2005-97, Microsoft Research, 2005.]] |
| [24] | T. Lev-Ami, N. Immerman, T. W. Reps, S. Sagiv, S. Srivastava, and G. Yorsh. Simulating reachability using first-order logic with applications to verification of linked data structures. In CADE 05: Conference on Automated Deduction, volume 3632 of LNCS, pages 99-115. Springer-Verlag, 2005.]] 10.1007/11532231_8 · Zbl 1135.68556 |
| [25] | T. Lev-Ami and S. Sagiv. TVLA: A system for implementing static analyses. In SAS 00: Static Analysis Symposium, volume 1824 of LNCS, pages 280-301. Springer-Verlag, 2000.]] · Zbl 0966.68580 |
| [26] | R. Manevich, E. Yahav, G. Ramalingam, and M. Sagiv. Predicate abstraction and canonical abstraction for singly-linked lists. In VMCAI 05: Verification, Model Checking and Abstract Interpretation, volume 3148 of LNCS, pages 181-198. Springer-Verlag, 2005.]] 10.1007/978-3-540-30579-8_13 · Zbl 1111.68398 |
| [27] | S. McPeak and G. C. Necula. Data structure specifications via local equality axioms. In Computer-Aided Verification (CAV ’05), volume 3576 of LNCS, pages 476-490. Springer-Verlag, 2005.]] 10.1007/11513988_47 · Zbl 1081.68584 |
| [28] | A. Møller and M. I. Schwartzbach. The pointer assertion logic engine. In PLDI 01: Programming Language Design and Implementation, pages 221-231, 2001.]] 10.1145/378795.378851 |
| [29] | M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient SAT solver. In 38th Design Automation Conference (DAC ’01), 2001.]] 10.1145/378239.379017 |
| [30] | G. Nelson and D. C. Oppen. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems (TOPLAS), 2(1):245-257, 1979.]] 10.1145/357073.357079 · Zbl 0452.68013 |
| [31] | G. Nelson and F. F. Yao. Solving reachability constraints for linear lists, 1982. Unpublished manuscript.]] |
| [32] | G. Nelson. Verifying reachability invariants of linked structures. In POPL 83: Principles of Programming Languages, pages 38-47. ACM Press, 1983.]] 10.1145/567067.567073 |
| [33] | P. W. O’Hearn, J. C. Reynolds, and H. Yang. Local reasoning about programs that alter data structures. In CSL 01: 15th International Workshop on Computer Science Logic, volume 2142 of LNCS, pages 1-19. Springer-Verlag, 2001.]] · Zbl 0999.68045 |
| [34] | P. W. O’Hearn, H. Yang, and J. C. Reynolds. Separation and information hiding. In POPL 04: Principles of Programming Languages, pages 268-280. ACM Press, 2004.]] 10.1145/964001.964024 · Zbl 1325.68069 |
| [35] | S. Ranise and C. Zarba. A decidable logic for pointer programs manipulating linked lists, 2004. Unpublished manuscript.]] |
| [36] | T. Reps, M. Sagiv, and A. Loginov. Finite differencing of logical formulas for static analysis. In ESOP 03: European Symposium on Programming, volume 2618 of LNCS, pages 380-398. Springer-Verlag, 2003.]] · Zbl 1032.68061 |
| [37] | J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS 02: Logic in Computer Science, pages 55-74. IEEE Computer Society Press, 2002.]] |
| [38] | R. Wilhelm S. Sagiv, T. W. Reps. Solving shape-analysis problems in languages with destructive updating. ACM Transactions on Programming Languages and Systems (TOPLAS), 20(1):1-50, 1998.]] 10.1145/271510.271517 |
| [39] | M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. In POPL 99: Principles of Programming Languages, pages 105-118. ACM Press, 1999.]] 10.1145/292540.292552 |
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.
