{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,6]],"date-time":"2025-02-06T05:40:11Z","timestamp":1738820411059,"version":"3.37.0"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540938996"},{"type":"electronic","value":"9783540939009"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-93900-9_24","type":"book-chapter","created":{"date-parts":[[2008,12,15]],"date-time":"2008-12-15T09:35:59Z","timestamp":1229333759000},"page":"290-304","source":"Crossref","is-referenced-by-count":22,"title":["A Scalable Memory Model for Low-Level Code"],"prefix":"10.1007","author":[{"given":"Zvonimir","family":"Rakamari\u0107","sequence":"first","affiliation":[]},{"given":"Alan J.","family":"Hu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"24_CR1","unstructured":"The DDVerify verification tool (2007) (Cited: August 15, 2008), http:\/\/www.verify.ethz.ch\/ddverify\/"},{"key":"24_CR2","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI), pp. 203\u2013213 (2001)","DOI":"10.1145\/378795.378846"},{"key":"24_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M. Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 364\u2013387. Springer, Heidelberg (2006)"},{"key":"24_CR4","doi-asserted-by":"crossref","unstructured":"Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. In: Workshop on Program Analysis For Software Tools and Engineering (PASTE), pp. 82\u201387 (2005)","DOI":"10.1145\/1108792.1108813"},{"key":"24_CR5","series-title":"Lecture Notes in Computer Science","first-page":"49","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M. Barnett","year":"2006","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: Barthe, G., Gr\u00e9goire, B., Huisman, M., Lanet, J.-L. (eds.) CASSIS 2005. LNCS, vol.\u00a03956, pp. 49\u201369. Springer, Heidelberg (2006)"},{"key":"24_CR6","doi-asserted-by":"crossref","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI), pp. 196\u2013207 (2003)","DOI":"10.1145\/780822.781153"},{"key":"24_CR7","first-page":"23","volume":"7","author":"R.M. Burstall","year":"1972","unstructured":"Burstall, R.M.: Some techniques for proving correctness of programs which alter data structures. Machine Intelligence\u00a07, 23\u201350 (1972)","journal-title":"Machine Intelligence"},{"key":"24_CR8","doi-asserted-by":"crossref","unstructured":"Chaki, S., Clarke, E.M., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. In: Intl. Conf. on Software Engineering (ICSE), pp. 385\u2013395 (2003)","DOI":"10.1109\/ICSE.2003.1201217"},{"key":"24_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-540-71209-1_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","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)"},{"key":"24_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kr\u00f6ning, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"issue":"2-3","key":"24_CR11","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":"24_CR12","doi-asserted-by":"crossref","unstructured":"Condit, J., Hackett, B., Lahiri, S., Qadeer, S.: Unifying type checking and property checking for low-level code. In: ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, POPL (to appear, 2009)","DOI":"10.1145\/1594834.1480921"},{"key":"24_CR13","doi-asserted-by":"crossref","unstructured":"Condit, J., Harren, M., Mcpeak, S., Necula, G.C., Weimer, W.: Cured in the real world. In: ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI), pp. 232\u2013244 (2003)","DOI":"10.1145\/780822.781157"},{"key":"24_CR14","doi-asserted-by":"crossref","unstructured":"Currie, D.W., Hu, A.J., Rajan, S., Fujita, M.: Automatic formal verification of DSP software. In: 37th Design Automation Conference, pp. 130\u2013135. ACM\/IEEE (2000)","DOI":"10.1145\/337292.337339"},{"key":"24_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"24_CR16","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":"24_CR17","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":"24_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-540-30482-1_10","volume-title":"Formal Methods and Software Engineering","author":"J.-C. Filli\u00e2tre","year":"2004","unstructured":"Filli\u00e2tre, J.-C., 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)"},{"key":"24_CR19","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: ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI), pp. 234\u2013245 (2002)","DOI":"10.1145\/512529.512558"},{"key":"24_CR20","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages (POPL), pp. 58\u201370 (2002)","DOI":"10.1145\/503272.503279"},{"key":"24_CR21","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: Intl. Conf. on Computer Design (ICCD), pp. 297\u2013308 (2005)","DOI":"10.1109\/ICCD.2005.77"},{"key":"24_CR22","doi-asserted-by":"crossref","unstructured":"Lattner, C., Adve, V.: LLVM: A compilation framework for lifelong program analysis & transformation. In: Symp. on Code Generation and Optimization (CGO), pp. 75\u201388 (2004)","DOI":"10.1109\/CGO.2004.1281665"},{"key":"24_CR23","doi-asserted-by":"crossref","unstructured":"Lattner, C., Lenharth, A., Adve, V.S.: Making context-sensitive points-to analysis with heap cloning practical for the real world. In: ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI), pp. 278\u2013289 (2007)","DOI":"10.1145\/1250734.1250766"},{"key":"24_CR24","doi-asserted-by":"crossref","unstructured":"Min\u00e9, A.: Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics. In: ACM SIGPLAN\/SIGBED Conf. on Languages, Compilers, and Tools for Embedded Systems (LCTES), pp. 54\u201363 (2006)","DOI":"10.1145\/1159974.1134659"},{"key":"24_CR25","unstructured":"Moy, Y.: Union and cast in deductive verification. In: C\/C++ Verification Workshop (CCV), pp. 1\u201316 (2007)"},{"key":"24_CR26","doi-asserted-by":"crossref","unstructured":"Rakamari\u0107, Z., Hu, A.J.: Automatic inference of frame axioms using static analysis. In: IEEE\/ACM Intl. Conf. on Automated Software Engineering (ASE), pp. 89\u201398 (2008)","DOI":"10.1109\/ASE.2008.19"},{"key":"24_CR27","unstructured":"Schulte, W., Xia, S., Smans, J., Piessens, F.: A glimpse of a verifying C compiler (extended abstract). In: C\/C++ Verification Workshop (2007)"},{"key":"24_CR28","doi-asserted-by":"crossref","unstructured":"Siff, M., Chandra, S., Ball, T., Kunchithapadam, K., Reps, T.W.: Coping with type casts in C. In: European Software Engineering Conf.\/ACM SIGSOFT Symp. on the Foundations of Software Engineering (ESEC\/FSE), pp. 180\u2013198 (1999)","DOI":"10.1007\/3-540-48166-4_12"},{"key":"24_CR29","doi-asserted-by":"crossref","unstructured":"Witkowski, T., Blanc, N., Kroening, D., Weissenbacher, G.: Model checking concurrent linux device drivers. In: IEEE\/ACM Intl. Conf. on Automated Software Engineering (ASE), pp. 501\u2013504 (2007)","DOI":"10.1145\/1321631.1321719"}],"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-93900-9_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,6]],"date-time":"2025-02-06T05:20:02Z","timestamp":1738819202000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-93900-9_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540938996","9783540939009"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-93900-9_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}