{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:00:14Z","timestamp":1725494414421},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540697350"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-69738-1_8","type":"book-chapter","created":{"date-parts":[[2007,11,12]],"date-time":"2007-11-12T12:58:07Z","timestamp":1194872287000},"page":"106-121","source":"Crossref","is-referenced-by-count":14,"title":["An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures"],"prefix":"10.1007","author":[{"given":"Zvonimir","family":"Rakamari\u0107","sequence":"first","affiliation":[]},{"given":"Jesse","family":"Bingham","sequence":"additional","affiliation":[]},{"given":"Alan J.","family":"Hu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11609773_14","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"J. Bingham","year":"2005","unstructured":"Bingham, J., Rakamari\u0107, Z.: A Logic and Decision Procedure for Predicate Abstraction of Heap-Manipulating Programs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, Springer, Heidelberg (2005)"},{"key":"8_CR2","unstructured":"Bingham, J., Rakamari\u0107, Z.: A Logic and Decision Procedure for Predicate Abstraction of Heap-Manipulating Programs, UBC Dept. Comp. Sci. Tech Report TR-2005-19 (2005), http:\/\/www.cs.ubc.ca\/cgi-bin\/tr\/2005\/TR-2005-19"},{"key":"8_CR3","unstructured":"Rakamari\u0107, Z., Bingham, J., Hu, A.J.: A Better Logic and Decision Procedure for Predicate Abstraction of Heap-Manipulating Programs, UBC Dept. Comp. Sci. Tech Report TR-2006-02 (2006), http:\/\/www.cs.ubc.ca\/cgi-bin\/tr\/2006\/TR-2006-02"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11823230_16","volume-title":"Static Analysis","author":"A. Gotsman","year":"2006","unstructured":"Gotsman, A., Berdine, J., Cook, B.: Interprocedural Shape Analysis with Separated Heap Abstractions. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134, Springer, Heidelberg (2006)"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science","author":"J. Berdine","year":"2004","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: A Decidable Fragment of Separation Logic. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol.\u00a03328, Springer, Heidelberg (2004)"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Smallfoot: Modular Automatic Assertion Checking with Separation Logic. In: Intl. Symp. on Formal Methods for Components and Objects, FMCO (2006)","DOI":"10.1007\/11804192_6"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"I. Balaban","year":"2005","unstructured":"Balaban, I., Pnueli, A., Zuck, L.: Shape Analysis by Predicate Abstraction. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, Springer, Heidelberg (2005)"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Qadeer, S.: Predicate Abstraction for Software Verification. In: Symp. on Principles of Programming Languages, POPL (2002)","DOI":"10.1145\/503272.503291"},{"key":"8_CR9","unstructured":"Nelson, G.: Techniques for Program Verification. PhD thesis, Stanford University (1979)"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Nelson, G.: Verifying Reachability Invariants of Linked Structures. In: Symp. on Principles of Programming Languages, POPL (1983)","DOI":"10.1145\/567067.567073"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49099-X_2","volume-title":"Programming Languages and Systems","author":"M. Benedikt","year":"1999","unstructured":"Benedikt, M., Reps, T., Sagiv, M.: A Decidable Logic for Describing Linked Data Structures. In: Swierstra, S.D. (ed.) ESOP 1999 and ETAPS 1999. LNCS, vol.\u00a01576, Springer, Heidelberg (1999)"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/b98118","volume-title":"Computer Science Logic","author":"N. Immerman","year":"2004","unstructured":"Immerman, N., et al.: The Boundary Between Decidability and Undecidability for Transitive Closure Logics. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol.\u00a03210, Springer, Heidelberg (2004)"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: Symp. on Principles of Programming Languages, POPL (1977)","DOI":"10.1145\/512950.512973"},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D. Dams","year":"2002","unstructured":"Dams, D., Namjoshi, K.S.: Shape Analysis Through Predicate Abstraction and Model Checking. In: Zuck, L.D., et al. (eds.) VMCAI 2003. LNCS, vol.\u00a02575, Springer, Heidelberg (2002)"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of Abstract State Graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, Springer, Heidelberg (1997)"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48683-6_16","volume-title":"Computer Aided Verification","author":"S. Das","year":"1999","unstructured":"Das, S., Dill, D.L., Park, S.: Experience with Predicate Abstraction. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, Springer, Heidelberg (1999)"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy Abstraction. In: Symp. on Principles of Programming Languages, POPL (2002)","DOI":"10.1145\/503272.503279"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"M\u00f8ller, A., Schwartzbach, M.I.: The Pointer Assertion Logic Engine. In: Conf. on Programming Language Design and Implementation, PLDI (2001)","DOI":"10.1145\/378795.378851"},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11609773_11","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T. Wies","year":"2005","unstructured":"Wies, T., et al.: Field Constraint Analysis. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, Springer, Heidelberg (2005)"},{"key":"8_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36575-3_26","volume-title":"Programming Languages and Systems","author":"T. Reps","year":"2003","unstructured":"Reps, T., Sagiv, M., Loginov, A.: Finite Differencing of Logical Formulas for Static Analysis. In: Degano, P. (ed.) ESOP 2003 and ETAPS 2003. LNCS, vol.\u00a02618, Springer, Heidelberg (2003)"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11690634_7","volume-title":"Foundations of Software Science and Computation Structures","author":"G. Yorsh","year":"2006","unstructured":"Yorsh, G., et al.: A Logic of Reachable Patterns in Linked Data-Structures. In: Aceto, L., Ing\u00f3lfsd\u00f3ttir, A. (eds.) FOSSACS 2006 and ETAPS 2006. LNCS, vol.\u00a03921, Springer, Heidelberg (2006)"},{"key":"8_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/b98118","volume-title":"Computer Aided Verification","author":"N. Immerman","year":"2004","unstructured":"Immerman, N., et al.: Verification via Structure Simulation. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, Springer, Heidelberg (2004)"},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Qadeer, S.: Verifying Properties of Well-Founded Linked Lists. In: Symp. on Principles of Programming Languages, POPL (2006)","DOI":"10.1145\/1111037.1111048"},{"key":"8_CR24","series-title":"Lecture Notes in Computer Science","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R. Manevich","year":"2005","unstructured":"Manevich, R., et al.: Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, Springer, Heidelberg (2005)"},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"A. Loginov","year":"2005","unstructured":"Loginov, A., Reps, T.W., Sagiv, S.: Abstraction Refinement via Inductive Learning. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, Springer, Heidelberg (2005)"},{"key":"8_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Distefano","year":"2006","unstructured":"Distefano, D., O\u2019Hearn, P.W., Yang, H.: A Local Shape Analysis Based on Separation Logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol.\u00a03920, Springer, Heidelberg (2006)"},{"key":"8_CR27","doi-asserted-by":"crossref","unstructured":"Ishtiaq, S., O\u2019Hearn, P.W.: BI as an Assertion Language for Mutable Data Structures. In: Symp. on Principles of Programming Languages, POPL (2001)","DOI":"10.1145\/360204.375719"},{"key":"8_CR28","unstructured":"Magill, S., Nanevski, A., Clarke, E.M., Lee, P.: Inferring Invariants in Separation Logic for Imperative List-processing Programs. In: Workshop on Semantics, Program Analysis, and Computing Environments for Memory Management, SPACE (2006)"},{"key":"8_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_49","volume-title":"Computer Aided Verification","author":"T. Lev-Ami","year":"2006","unstructured":"Lev-Ami, T., Immerman, N., Sagiv, M.: Abstraction for Shape Analysis with Fast and Precise Transformers. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, Springer, Heidelberg (2006)"},{"key":"8_CR30","doi-asserted-by":"crossref","unstructured":"Klarlund, N., M\u00f8ller, A., Schwartzbach, M.I.: MONA Implementation Secrets. In: Conf. on Implementation and Application of Automata, CIAA (2000)","DOI":"10.7146\/brics.v7i40.20206"},{"key":"8_CR31","series-title":"Lecture Notes in Computer Science","volume-title":"Static Analysis","author":"T. Lev-Ami","year":"2000","unstructured":"Lev-Ami, T., Sagiv, M.: TVLA: A System for Implementing Static Analyses. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol.\u00a01824, Springer, Heidelberg (2000)"},{"key":"8_CR32","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic Predicate Abstraction of C Programs. In: Conf. on Programming Language Design and Implementation, PLDI (2001)","DOI":"10.1145\/378795.378846"},{"key":"8_CR33","series-title":"Lecture Notes in Computer Science","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Yorsh","year":"2004","unstructured":"Yorsh, G., Reps, T., Sagiv, M.: Symbolically Computing Most-Precise Abstract Operations for Shape Analysis. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, Springer, Heidelberg (2004)"},{"key":"8_CR34","doi-asserted-by":"crossref","unstructured":"Ranise, S., Zarba, C.G.: A Theory of Singly-Linked Lists and its Extensible Decision Procedure. In: IEEE Int. Conf. on Software Engineering and Formal Methods, SEFM (2006)","DOI":"10.1109\/SEFM.2006.7"},{"key":"8_CR35","series-title":"Lecture Notes in Computer Science","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K.L. McMillan","year":"2005","unstructured":"McMillan, K.L.: Applications of Craig Interpolants in Model Checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, Springer, Heidelberg (2005)"},{"issue":"10","key":"8_CR36","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An Axiomatic Basis for Computer Programming. Communications of the ACM\u00a012(10), 576\u2013583 (1969)","journal-title":"Communications of the ACM"},{"issue":"2","key":"8_CR37","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems (TOPLAS)\u00a08(2), 244\u2013263 (1986)","journal-title":"ACM Transactions on Programming Languages and Systems (TOPLAS)"},{"key":"8_CR38","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Deduction \u2013 CADE-20","author":"T. Lev-Ami","year":"2005","unstructured":"Lev-Ami, T., et al.: Simulating Reachability using First-Order Logic with Applications to Verification of Linked Data Structures. In: Nieuwenhuis, R. (ed.) Automated Deduction \u2013 CADE-20. LNCS (LNAI), vol.\u00a03632, Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69738-1_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T04:45:12Z","timestamp":1620017112000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69738-1_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540697350"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69738-1_8","relation":{},"subject":[]}}