{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:13:32Z","timestamp":1763468012314},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540242970"},{"type":"electronic","value":"9783540305798"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-30579-8_13","type":"book-chapter","created":{"date-parts":[[2010,12,20]],"date-time":"2010-12-20T16:45:34Z","timestamp":1292863534000},"page":"181-198","source":"Crossref","is-referenced-by-count":53,"title":["Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists"],"prefix":"10.1007","author":[{"given":"Roman","family":"Manevich","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"E.","family":"Yahav","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"G.","family":"Ramalingam","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.: Automatic predicate abstraction of C programs. In: Proc. Conf. on Prog. Lang. Design and Impl., pp. 203\u2013213 (June 2001)","DOI":"10.1145\/378795.378846"},{"key":"13_CR2","unstructured":"Ball, T., Rajamani, S.: Generating abstract explanations of spurious counterexamples in c programs. Report MSR-TR-2002-09, Microsoft Research, Microsoft Redmond (January 2002), http:\/\/research.microsoft.com\/slam\/"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"Benedikt, M., Reps, T., Sagiv, M.: A decidable logic for describing linked data structures. In: Proceedings of the 1999 European Symposium On Programming, pp. 2\u201319 (March 1999)","DOI":"10.1007\/3-540-49099-X_2"},{"key":"13_CR4","series-title":"ACMSIGPLAN Notices","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1145\/781131.781153","volume-title":"Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLDI 2003)","author":"B. Blanchet","year":"2003","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Mine, M., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: Fenwick, J.J.B., Norris, C. (eds.) Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLDI 2003), June 9\u201311. ACMSIGPLAN Notices, vol.\u00a038(5), pp. 196\u2013207. ACM Press, New York (2003)"},{"key":"13_CR5","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1145\/604131.604142","volume-title":"Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages","author":"V.T. Chakaravarthy","year":"2003","unstructured":"Chakaravarthy, V.T.: New results on the computability and complexity of points\u2013to analysis. In: Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 115\u2013125. ACM Press, New York (2003)"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E. Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"13_CR7","first-page":"269","volume-title":"Proc. Symp. on Principles of Prog. Languages","author":"P. Cousot","year":"1979","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proc. Symp. on Principles of Prog. Languages, pp. 269\u2013282. ACM Press, New York (1979)"},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/3-540-36384-X_25","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., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol.\u00a02575, pp. 310\u2013324. Springer, Heidelberg (2002)"},{"key":"13_CR9","first-page":"230","volume-title":"Proc. Conf. on Prog. Lang. Design and Impl.","author":"A. Deutsch","year":"1994","unstructured":"Deutsch, A.: Interprocedural may-alias analysis for pointers: Beyond k-limiting. In: Proc. Conf. on Prog. Lang. Design and Impl., pp. 230\u2013241. ACM Press, New York (1994)"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"Gopan, D., DiMaio, F., Dor, N., Reps, T., Sagiv, M.: Numeric domains with summarized dimensions. In: Tools and Algs. for the Construct. and Anal. of Syst., pp. 512\u2013529 (2004)","DOI":"10.1007\/978-3-540-24730-2_38"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","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, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Symposium on Principles of Programming Languages, pp. 58\u201370 (2002)","DOI":"10.1145\/503272.503279"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., Yorsh, G.: The boundary between decidability and undecidability for transitive closure logics. In: Proc. Computer Science Logic (2004) (to appear)","DOI":"10.1007\/978-3-540-30124-0_15"},{"issue":"3","key":"13_CR14","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1145\/373243.375719","volume":"36","author":"S.S. Ishtiaq","year":"2001","unstructured":"Ishtiaq, S.S., O\u2019Hearn, P.W.: BI as an assertion language for mutable data structures. ACM SIGPLAN Notices\u00a036(3), 14\u201326 (2001)","journal-title":"ACM SIGPLAN Notices"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"Jensen, J., Joergensen, M., Klarlund, N., Schwartzbach, M.: Automatic verification of pointer programs using monadic second-order logic. In: Proc. Conf. on Prog. Lang. Design and Impl. (1997)","DOI":"10.1145\/258915.258936"},{"key":"13_CR16","first-page":"102","volume-title":"Program Flow Analysis: Theory and Applications, ch. 4","author":"N. Jones","year":"1981","unstructured":"Jones, N., Muchnick, S.: Flow analysis and optimization of Lisp-like structures. In: Muchnick, S., Jones, N. (eds.) Program Flow Analysis: Theory and Applications, ch. 4, pp. 102\u2013131. Prentice-Hall, Englewood Cliffs (1981)"},{"key":"13_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-540-45099-3_15","volume-title":"Static Analysis","author":"T. Lev-Ami","year":"2000","unstructured":"Lev-Ami, T., Sagiv, M.: TVLA: A framework for Kleene based static analysis. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol.\u00a01824, pp. 280\u2013301. Springer, Heidelberg (2000)"},{"key":"13_CR18","doi-asserted-by":"crossref","unstructured":"Manevich, R., Yahav, E., Ramalingam, G., Sagiv, M.: Predicate abstraction and canonical abstraction for singly-linked lists. Technical Report TR-2005-01-191212, Tel Aviv University (2005)","DOI":"10.1007\/978-3-540-30579-8_13"},{"key":"13_CR19","unstructured":"Microsoft Research. The SLAM project (2001), http:\/\/research.microsoft.com\/slam\/"},{"issue":"1","key":"13_CR20","first-page":"1","volume":"141","author":"M. Rabin","year":"1969","unstructured":"Rabin, M.: Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc.\u00a0141(1), 1\u201335 (1969)","journal-title":"Trans. Amer. Math. Soc."},{"key":"13_CR21","doi-asserted-by":"crossref","unstructured":"Ramalingam, G., Warshavsky, A., Field, J., Goyal, D., Sagiv, M.: Deriving specialized program analyses for certifying component-client conformance. In: Proc. Conf. on Prog. Lang. Design and Impl., vol.\u00a037(5), pp. 83\u201394 (June 2002)","DOI":"10.1145\/512529.512540"},{"key":"13_CR22","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-540-24622-0_21","volume-title":"Proc. Verification, Model Checking, and Abstract Interpretation","author":"T. Reps","year":"2004","unstructured":"Reps, T., Sagiv, M., Yorsh, G.: Symbolic implementation of the best transformer. In: Proc. Verification, Model Checking, and Abstract Interpretation, pp. 252\u2013266. Springer, Heidelberg (2004)"},{"issue":"3","key":"13_CR23","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M. Sagiv","year":"2002","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Transactions on Programming Languages and Systems (TOPLAS)\u00a024(3), 217\u2013298 (2002)","journal-title":"ACM Transactions on Programming Languages and Systems (TOPLAS)"},{"key":"13_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_27","volume-title":"Static Analysis","author":"R. Shaham","year":"2003","unstructured":"Shaham, R., Yahav, E., Kolodner, E.K., Sagiv, M.: Establishing local temporal heap safety properties with applications to compile-time memory management. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694. Springer, Heidelberg (2003)"},{"key":"13_CR25","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1145\/996841.996846","volume-title":"Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation","author":"E. Yahav","year":"2004","unstructured":"Yahav, E., Ramalingam, G.: Verifying safety properties using separation and heterogeneous abstractions. In: Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, pp. 25\u201334. ACM Press, New York (2004)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30579-8_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:24:14Z","timestamp":1605759854000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30579-8_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540242970","9783540305798"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30579-8_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}