{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T04:51:49Z","timestamp":1725511909440},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540712084"},{"type":"electronic","value":"9783540712091"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-71209-1_4","type":"book-chapter","created":{"date-parts":[[2007,7,4]],"date-time":"2007-07-04T22:56:34Z","timestamp":1183589794000},"page":"19-33","source":"Crossref","is-referenced-by-count":33,"title":["A Reachability Predicate for Analyzing Low-Level Software"],"prefix":"10.1007","author":[{"given":"Shaunak","family":"Chatterjee","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shuvendu K.","family":"Lahiri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shaz","family":"Qadeer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zvonimir","family":"Rakamari\u0107","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"164","DOI":"10.1007\/978-3-540-30579-8_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"I. Balaban","year":"2005","unstructured":"Balaban, I., Pnueli, A., Zuck, L.D.: Shape analysis by predicate abstraction. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 164\u2013180. Springer, Heidelberg (2005)"},{"doi-asserted-by":"crossref","unstructured":"Ball, T., et al.: Automatic predicate abstraction of C programs. In: Programming Language Design and Implementation (PLDI \u201901), pp. 203\u2013213 (2001)","key":"4_CR2","DOI":"10.1145\/378795.378846"},{"key":"4_CR3","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1145\/1108792.1108813","volume-title":"ACM SIGPLAN-SIGSOFT Workshop on Program Analysis For Software Tools and Engineering (PASTE \u201905)","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. In: ACM SIGPLAN-SIGSOFT Workshop on Program Analysis For Software Tools and Engineering (PASTE \u201905), pp. 82\u201387. ACM Press, New York (2005)"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: Barthe, G., et al. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 49\u201369. Springer, Heidelberg (2005)"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/11609773_14","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"J. Bingham","year":"2005","unstructured":"Bingham, J.: 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":"4_CR6","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-59207-2","volume-title":"The Classical Decision Problem","author":"E. B\u00f6rger","year":"1997","unstructured":"B\u00f6rger, E., Gr\u00e4del, E., Gurevich, Y.: The Classical Decision Problem. Springer, Heidelberg (1997)"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/11823230_13","volume-title":"Static Analysis","author":"C. Calcagno","year":"2006","unstructured":"Calcagno, C., et al.: Beyond reachability: Shape abstraction in the presence of pointer arithmetic. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134, pp. 182\u2013203. Springer, Heidelberg (2006)"},{"unstructured":"Chatterjee, S., et al.: A reachability predicate for analyzing low-level software. Technical Report MSR-TR-2006-154, Microsoft Research (2006)","key":"4_CR8"},{"key":"4_CR9","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., et al.: Predicate Abstraction of ANSI\u2013C Programs using SAT. Formal Methods in System Design (FMSD)\u00a025, 105\u2013127 (2004)","journal-title":"Formal Methods in System Design (FMSD)"},{"doi-asserted-by":"crossref","unstructured":"Das, M., Lerner, S., Seigle, M.: ESP: Path-sensitive program verification in polynomial time. In: Programming Language Design and Implementation (PLDI \u201902), pp. 57\u201368 (2002)","key":"4_CR10","DOI":"10.1145\/512529.512538"},{"unstructured":"DeLine, R., Leino, K.R.M.: BoogiePL: A typed procedural language for checking object-oriented programs. Technical Report MSR-TR-2005-70, Microsoft Research (2005)","key":"4_CR11"},{"unstructured":"Detlefs, D.L., Nelson, G., Saxe, J.B.: Simplify: A theorem prover for program checking. Technical report, HPL-2003-148 (2003)","key":"4_CR12"},{"key":"4_CR13","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E.W. Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM\u00a018, 453\u2013457 (1975)","journal-title":"Communications of the ACM"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1007\/978-3-540-30482-1_10","volume-title":"Formal Methods and Software Engineering","author":"J. Filli\u00e2tre","year":"2004","unstructured":"Filli\u00e2tre, J., March\u00e9, C.: Multi-prover verification of C programs. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol.\u00a03308, pp. 15\u201329. Springer, Heidelberg (2004)"},{"doi-asserted-by":"crossref","unstructured":"Flanagan, C., et al.: Extended static checking for Java. In: Programming Language Design and Implementation (PLDI\u201902), pp. 234\u2013245 (2002)","key":"4_CR15","DOI":"10.1145\/512529.512558"},{"doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., et al.: Lazy abstraction. In: Principles of Programming Languages (POPL \u201902), Portland, Oregon, pp. 58\u201370 (2002)","key":"4_CR16","DOI":"10.1145\/503272.503279"},{"doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Qadeer, S.: Verifying properties of well-founded linked lists. In: Principles of Programming Languages (POPL \u201906), pp. 115\u2013126 (2006)","key":"4_CR17","DOI":"10.1145\/1111037.1111048"},{"key":"4_CR18","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1007\/11532231_8","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, pp. 99\u2013115. Springer, Heidelberg (2005)"},{"key":"4_CR19","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":"Static Analysis","author":"T. Lev-Ami","year":"2000","unstructured":"Lev-Ami, T., Sagiv, S.: TVLA: A system for implementing static analyses. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol.\u00a01824, pp. 280\u2013301. Springer, Heidelberg (2000)"},{"key":"4_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"476","DOI":"10.1007\/11513988_47","volume-title":"Computer Aided Verification","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)"},{"issue":"1","key":"4_CR21","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"2","author":"G. Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems (TOPLAS)\u00a02(1), 245\u2013257 (1979)","journal-title":"ACM Transactions on Programming Languages and Systems (TOPLAS)"},{"issue":"1","key":"4_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/271510.271517","volume":"20","author":"S. Sagiv","year":"1998","unstructured":"Sagiv, S., Reps, T.W., Wilhelm, R.: Solving shape-analysis problems in languages with destructive updating. ACM Transactions on Programming Languages and Systems (TOPLAS)\u00a020(1), 1\u201350 (1998)","journal-title":"ACM Transactions on Programming Languages and Systems (TOPLAS)"},{"doi-asserted-by":"crossref","unstructured":"Xie, Y., Aiken, A.: Scalable error detection using boolean satisfiability. In: Principles of Programming Languages (POPL \u201905), pp. 351\u2013363 (2005)","key":"4_CR23","DOI":"10.1145\/1040305.1040334"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71209-1_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:16:50Z","timestamp":1605763010000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71209-1_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540712084","9783540712091"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71209-1_4","relation":{},"subject":[]}}