{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,22]],"date-time":"2025-01-22T05:27:21Z","timestamp":1737523641397,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":41,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540755951"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-75596-8_18","type":"book-chapter","created":{"date-parts":[[2007,11,3]],"date-time":"2007-11-03T14:03:37Z","timestamp":1194098617000},"page":"237-252","source":"Crossref","is-referenced-by-count":10,"title":["Verifying Heap-Manipulating Programs in an SMT Framework"],"prefix":"10.1007","author":[{"given":"Zvonimir","family":"Rakamari\u0107","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roberto","family":"Bruttomesso","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alan J.","family":"Hu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alessandro","family":"Cimatti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"18_CR1","volume-title":"Studies in Logic and the Foundations of Mathematics","author":"W. Ackermann","year":"1954","unstructured":"Ackermann, W.: Solvable Cases of the Decision Problem. In: Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam (1954)"},{"key":"18_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1007\/978-3-540-73368-3_41","volume-title":"CAV 2007","author":"D. Babi\u0107","year":"2007","unstructured":"Babi\u0107, D., Hu, A.J.: Structural abstraction of software verification conditions. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 366\u2013378. Springer, Heidelberg (2007)"},{"key":"18_CR3","series-title":"Lecture Notes in Computer Science","volume-title":"VMCAI 2005","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":"18_CR4","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: PLDI. Conf. on Programming Language Design and Implementation, pp. 203\u2013213 (2001)","DOI":"10.1145\/378795.378846"},{"key":"18_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"CASSIS 2004","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, Springer, Heidelberg (2005)"},{"key":"18_CR6","series-title":"Lecture Notes in Computer Science","volume-title":"ESOP 1999","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. LNCS, vol.\u00a01576, Springer, Heidelberg (1999)"},{"key":"18_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"532","DOI":"10.1007\/11817963_48","volume-title":"CAV 2006","author":"D. Beyer","year":"2006","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G.: Lazy shape analysis. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 532\u2013546. Springer, Heidelberg (2006)"},{"key":"18_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"504","DOI":"10.1007\/978-3-540-73368-3_51","volume-title":"CAV 2007","author":"D. Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G.: Configurable software verification: Concretizing the convergence of model checking and program analysis. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 504\u2013518. Springer, Heidelberg (2007)"},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/11609773_14","volume-title":"VMCAI 2006","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, pp. 207\u2013221. Springer, Heidelberg (2005)"},{"key":"18_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"335","DOI":"10.1007\/11513988_34","volume-title":"CAV 2005","author":"M. Bozzano","year":"2005","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., Rossum, P.V., Ranise, S., Sebastiani, R.: Efficient satisfiability modulo theories via delayed theory combination. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 335\u2013349. Springer, Heidelberg (2005)"},{"key":"18_CR11","doi-asserted-by":"publisher","first-page":"1493","DOI":"10.1016\/j.ic.2005.05.011","volume":"204","author":"M. Bozzano","year":"2006","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., Rossum, P.V., Ranise, S., Sebastiani, R.: Efficient theory combination via boolean search. Information and Computation\u00a0204, 1493\u20131525 (2006)","journal-title":"Information and Computation"},{"key":"18_CR12","series-title":"Lecture Notes in Artificial Intelligence","first-page":"315","volume-title":"CADE 2005","author":"M. Bozzano","year":"2005","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., Rossum, P.V., Schulz, S., Sebastiani, R.: The MathSAT 3 system. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 315\u2013321. Springer, Heidelberg (2005)"},{"key":"18_CR13","series-title":"Lecture Notes in Artificial Intelligence","first-page":"527","volume-title":"LPAR 2006","author":"R. Bruttomesso","year":"2006","unstructured":"Bruttomesso, R., Cimatti, A., Franz\u00e9n, A., Griggio, A., Sebastiani, R.: Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: A comparative analysis. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol.\u00a04246, pp. 527\u2013541. Springer, Heidelberg (2006)"},{"key":"18_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"168","DOI":"10.1007\/978-3-540-73368-3_20","volume-title":"CAV 2007","author":"N. Charlton","year":"2007","unstructured":"Charlton, N., Huth, M.: Hector: Software model checking with cooperating analysis plugins. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 168\u2013172. Springer, Heidelberg (2007)"},{"key":"18_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1007\/978-3-540-71209-1_4","volume-title":"TACAS 2007","author":"S. Chatterjee","year":"2007","unstructured":"Chatterjee, S., Lahiri, S.K., Qadeer, S., Rakamari\u0107, Z.: A reachability predicate for analyzing low-level software. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 19\u201333. Springer, Heidelberg (2007)"},{"issue":"2-3","key":"18_CR16","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1023\/B:FORM.0000040025.89719.f3","volume":"25","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSI\u2013C programs using SAT. Formal Methods in System Design\u00a025(2-3), 105\u2013127 (2004)","journal-title":"Formal Methods in System Design"},{"key":"18_CR17","unstructured":"Detlefs, D., Nelson, G., Saxe, J.: Simplify: A theorem prover for program checking, Technical Report HPL-2003-148, HP Labs, Palo Alto, CA (2003)"},{"key":"18_CR18","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: PLDI. Conf. on Programming Language Design and Implementation, pp. 234\u2013245 (2002)","DOI":"10.1145\/512529.512558"},{"key":"18_CR19","series-title":"Lecture Notes in Computer Science","volume-title":"CAV 1997","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":"18_CR20","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL. Symp. on Principles of Programming Languages, pp. 58\u201370 (2002)","DOI":"10.1145\/503272.503279"},{"key":"18_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1007\/978-3-540-30124-0_15","volume-title":"CSL 2004","author":"N. Immerman","year":"2004","unstructured":"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.\u00a03210, pp. 160\u2013174. Springer, Heidelberg (2004)"},{"key":"18_CR22","doi-asserted-by":"crossref","unstructured":"Ivan\u010di\u0107, F., Shlyakhter, I., Gupta, A., Ganai, M.K., Kahlon, V., Wang, C., Yang, Z.: Model checking C programs using F-Soft. In: ICCD. Intl. Conf. on Computer Design, pp. 297\u2013308 (2005)","DOI":"10.1109\/ICCD.2005.77"},{"key":"18_CR23","doi-asserted-by":"crossref","unstructured":"Jensen, J.L., J\u00f8rgensen, M.E., Klarlund, N., Schwartzbach, M.I.: Automatic verification of pointer programs using monadic second-order logic. In: PLDI. Conf. on Programming Language Design and Implementation, pp. 226\u2013236 (1997)","DOI":"10.1145\/258915.258936"},{"key":"18_CR24","series-title":"Lecture Notes in Computer Science","volume-title":"CIAA 2000","author":"N. Klarlund","year":"2001","unstructured":"Klarlund, N., M\u00f8ller, A., Schwartzbach, M.I.: MONA implementation secrets. In: Yu, S., P\u0103un, A. (eds.) CIAA 2000. LNCS, vol.\u00a02088, Springer, Heidelberg (2001)"},{"key":"18_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"602","DOI":"10.1007\/978-3-540-71209-1_47","volume-title":"TACAS 2007","author":"S. Krsti\u0107","year":"2007","unstructured":"Krsti\u0107, S., Goel, A., Grundy, J., Tinelli, C.: Combined satisfiability modulo parametric theories. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 602\u2013617. Springer, Heidelberg (2007)"},{"key":"18_CR26","series-title":"Lecture Notes in Computer Science","first-page":"413","volume-title":"CAV 2006","author":"S.K. Lahiri","year":"2006","unstructured":"Lahiri, S.K., Nieuwenhuis, R., Oliveras, A.: SMT techniques for fast predicate abstraction. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 413\u2013426. Springer, Heidelberg (2006)"},{"key":"18_CR27","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Qadeer, S.: Verifying properties of well-founded linked lists. In: POPL. Symp. on Principles of Programming Languages, pp. 115\u2013126 (2006)","DOI":"10.1145\/1111037.1111048"},{"key":"18_CR28","unstructured":"Lahiri, S.K., Qadeer, S.: A decision procedure for well-founded reachability, Microsoft Research Tech Report MSR-TR-2007-43 (2007)"},{"key":"18_CR29","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"CADE 2005","author":"T. Lev-Ami","year":"2005","unstructured":"Lev-Ami, T., Immerman, N., Reps, T.W., Sagiv, M., Srivastava, S., Yorsh, G.: Simulating reachability using first-order logic with applications to verification of linked data structures. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, Springer, Heidelberg (2005)"},{"key":"18_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1007\/978-3-540-45099-3_15","volume-title":"SAS 2000","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, pp. 280\u2013301. Springer, Heidelberg (2000)"},{"key":"18_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1007\/978-3-540-30579-8_13","volume-title":"VMCAI 2005","author":"R. Manevich","year":"2005","unstructured":"Manevich, R., Yahav, E., Ramalingam, G., Sagiv, M.: Predicate abstraction and canonical abstraction for singly-linked lists. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 181\u2013198. Springer, Heidelberg (2005)"},{"key":"18_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1007\/978-3-540-40007-3_24","volume-title":"10th Anniversary Colloquium of UNU\/IIST","author":"Z. Manna","year":"2003","unstructured":"Manna, Z., Zarba, C.G.: Combining decision procedures. In: Aichernig, B.K., Maibaum, T.S.E. (eds.) Formal Methods at the Crossroads. From Panacea to Foundational Support. LNCS, vol.\u00a02757, pp. 381\u2013422. Springer, Heidelberg (2003)"},{"key":"18_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"476","DOI":"10.1007\/11513988_47","volume-title":"CAV 2005","author":"S. McPeak","year":"2005","unstructured":"McPeak, S., Necula, G.C.: Data structure specifications via local equality axioms. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 476\u2013490. Springer, Heidelberg (2005)"},{"key":"18_CR34","doi-asserted-by":"crossref","unstructured":"M\u00f8ller, A., Schwartzbach, M.I.: The pointer assertion logic engine. In: PLDI. Conf. on Programming Language Design and Implementation, pp. 221\u2013231 (2001)","DOI":"10.1145\/378795.378851"},{"key":"18_CR35","unstructured":"Nelson, G.: Techniques for program verification. PhD thesis, Stanford University (1979)"},{"key":"18_CR36","doi-asserted-by":"crossref","unstructured":"Nelson, G.: Verifying reachability invariants of linked structures. In: POPL. Symp. on Principles of Programming Languages, pp. 38\u201347 (1983)","DOI":"10.1145\/567067.567073"},{"issue":"2","key":"18_CR37","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst.\u00a01(2), 245\u2013257 (1979)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"18_CR38","unstructured":"Rakamari\u0107, Z., Bingham, J., Hu, A.: 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":"18_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"106","DOI":"10.1007\/978-3-540-69738-1_8","volume-title":"VMCAI 2007","author":"Z. Rakamari\u0107","year":"2007","unstructured":"Rakamari\u0107, Z., Bingham, J., Hu, A.J.: An inference-rule-based decision procedure for verification of heap-manipulating programs with mutable data and cyclic data structures. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 106\u2013121. Springer, Heidelberg (2007)"},{"key":"18_CR40","doi-asserted-by":"crossref","unstructured":"Ranise, S., Zarba, C.G.: A theory of singly-linked lists and its extensible decision procedure. In: SEFM. IEEE Intl. Conf. on Software Engineering and Formal Methods (2006)","DOI":"10.1109\/SEFM.2006.7"},{"key":"18_CR41","series-title":"Lecture Notes in Computer Science","volume-title":"FOSSACS 2006","author":"G. Yorsh","year":"2006","unstructured":"Yorsh, G., Rabinovich, A., Sagiv, M., Meyer, A., Bouajjani, A.: A logic of reachable patterns in linked data-structures. In: Aceto, L., Ing\u00f3lfsd\u00f3ttir, A. (eds.) FOSSACS 2006. LNCS, vol.\u00a03921, Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-75596-8_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,22]],"date-time":"2025-01-22T02:31:10Z","timestamp":1737513070000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-75596-8_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540755951"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-75596-8_18","relation":{},"subject":[]}}