{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T07:18:30Z","timestamp":1781075910602,"version":"3.54.1"},"reference-count":50,"publisher":"Springer Science and Business Media LLC","issue":"2-4","license":[{"start":{"date-parts":[[2009,4,1]],"date-time":"2009-04-01T00:00:00Z","timestamp":1238544000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2009,4]]},"DOI":"10.1007\/s10817-009-9120-2","type":"journal-article","created":{"date-parts":[[2009,4,1]],"date-time":"2009-04-01T08:49:15Z","timestamp":1238575755000},"page":"125-187","source":"Crossref","is-referenced-by-count":20,"title":["Formal Verification of C Systems Code"],"prefix":"10.1007","volume":"42","author":[{"given":"Harvey","family":"Tuch","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2009,4,2]]},"reference":[{"key":"9120_CR1","unstructured":"Programming languages\u2014C. Technical report 9899:TC2, ISO\/IEC JTC1\/SC22\/WG14 (2005)"},{"key":"9120_CR2","first-page":"5","volume-title":"Proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2007). Lecture Notes in Computer Science, vol. 4732","author":"AW Appel","year":"2007","unstructured":"Appel, A.W., Blazy, S.: Separation logic for small-step Cminor. In: Schneider, K., Brandt, J. (eds.) Proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2007). Lecture Notes in Computer Science, vol. 4732, pp. 5\u201321. Springer, New York (2007)"},{"key":"9120_CR3","first-page":"103","volume-title":"Proceedings of the 8th International SPIN Workshop on Model Checking Software. Lecture Notes in Computer Science, vol. 2057","author":"T Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: Dwyer, M.B. (ed.) Proceedings of the 8th International SPIN Workshop on Model Checking Software. Lecture Notes in Computer Science, vol. 2057, pp. 103\u2013122. Springer, New York (2001)"},{"key":"9120_CR4","first-page":"97","volume-title":"Proceedings of the 24th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2004). Lecture Notes in Computer Science, vol. 3328","author":"J Berdine","year":"2004","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.: A decidable fragment of separation logic. In: Lodaya, K., Mahajan, M. (eds.) Proceedings of the 24th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2004). Lecture Notes in Computer Science, vol. 3328, pp. 97\u2013109. Springer, New York (2004)"},{"issue":"3","key":"9120_CR5","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1016\/0167-6423(89)90002-6","volume":"12","author":"A Bijlsma","year":"1989","unstructured":"Bijlsma, A.: Calculating with pointers. Sci. Comput. Program 12(3), 191\u2013205 (1989)","journal-title":"Sci. Comput. Program"},{"issue":"1","key":"9120_CR6","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1016\/S1571-0661(05)80452-9","volume":"59","author":"M Blume","year":"2001","unstructured":"Blume, M.: No-longer-foreign: teaching an ML compiler to speak C \u201cnatively\u201d. Electron. Notes Theoret. Comput. Sci. 59(1), 36\u201352 (2001)","journal-title":"Electron. Notes Theoret. Comput. Sci."},{"key":"9120_CR7","first-page":"102","volume-title":"Proceedings of the 5th International Conference on Mathematics of Program Construction (MPC 2000). Lecture Notes in Computer Science, vol. 1837","author":"R Bornat","year":"2000","unstructured":"Bornat, R.: Proving pointer programs in Hoare logic. In: Backhouse, R.C., Oliveira, J.N. (eds.) Proceedings of the 5th International Conference on Mathematics of Program Construction (MPC 2000). Lecture Notes in Computer Science, vol. 1837, pp. 102\u2013126. Springer, New York (2000)"},{"key":"9120_CR8","first-page":"23","volume-title":"Machine Intelligence, vol. 7","author":"R Burstall","year":"1972","unstructured":"Burstall, R.: Some techniques for proving correctness of programs which alter data structures. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, vol. 7, pp. 23\u201350. Edinburgh University Press, Edinburgh (1972)"},{"key":"9120_CR9","first-page":"182","volume-title":"Proceedings of the 13th International Symposium on Static Analysis (SAS 2006). Lecture Notes in Computer Science, vol. 4134","author":"C Calcagno","year":"2006","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Beyond reachability: shape abstraction in the presence of pointer arithmetic. In: Yi, K. (ed.) Proceedings of the 13th International Symposium on Static Analysis (SAS 2006). Lecture Notes in Computer Science, vol. 4134, pp. 182\u2013203. Springer, New York (2006)"},{"key":"9120_CR10","first-page":"108","volume-title":"Proceedings of the 21st Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2001). Lecture Notes in Computer Science, vol. 2245","author":"C Calcagno","year":"2001","unstructured":"Calcagno, C., Yang, H., O\u2019Hearn, P.W.: Computability and complexity results for a spatial assertion language for data structures. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) Proceedings of the 21st Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2001). Lecture Notes in Computer Science, vol. 2245, pp. 108\u2013119. Springer, New York (2001)"},{"key":"9120_CR11","volume-title":"The logic of aliasing. Technical report STAN-CS-79-740","author":"R Cartwright","year":"1979","unstructured":"Cartwright, R., Oppen, D.C.: The logic of aliasing. Technical report STAN-CS-79-740, Stanford University, Stanford (1979)"},{"key":"9120_CR12","unstructured":"Cock, D.: Bitfields and tagged unions in C: verification through automatic generation. In: Beckert, B., Klein, G. (eds.) Proceedings of the 5th International Verification Workshop in connection with IJCAR 2008, vol. 372 of CEUR Workshop Proceedings (2008). CEUR-WS.org"},{"key":"9120_CR13","first-page":"15","volume-title":"Proceedings of the 6th International Conference on Formal Methods and Software Engineering (ICFEM 2004). Lecture Notes in Computer Science, vol. 3308","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.) Proceedings of the 6th International Conference on Formal Methods and Software Engineering (ICFEM 2004). Lecture Notes in Computer Science, vol. 3308, pp. 15\u201329. Springer, New York (2004)"},{"key":"9120_CR14","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1145\/512529.512539","volume-title":"Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation. SIGPLAN Notices, vol. 37","author":"S Hallem","year":"2002","unstructured":"Hallem, S., Chelf, B., Xie, Y., Engler, D.R.: A system and language for building system-specific, static analyses. In: Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation. SIGPLAN Notices, vol. 37, pp. 69\u201382. ACM, New York (2002)"},{"key":"9120_CR15","first-page":"114","volume-title":"Proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2005). Lecture Notes in Computer Science, vol. 3603","author":"J Harrison","year":"2005","unstructured":"Harrison, J.: A HOL theory of Euclidean space. In: Hurd, J., Melham, T.F. (eds.) Proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2005). Lecture Notes in Computer Science, vol. 3603, pp. 114\u2013129. Springer, New York (2005)"},{"key":"9120_CR16","first-page":"235","volume-title":"Proceedings of the 10th International SPIN Workshop on Model Checking Software (SPIN 2003). Lecture Notes in Computer Science, vol. 2648","author":"TA Henzinger","year":"2003","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with BLAST. In: Ball, T., Rajamani, S.K. (eds.) Proceedings of the 10th International SPIN Workshop on Model Checking Software (SPIN 2003). Lecture Notes in Computer Science, vol. 2648, pp. 235\u2013239. Springer, New York (2003)"},{"key":"9120_CR17","doi-asserted-by":"crossref","unstructured":"Hohmuth, M., Tews, H., Stephens, S.G.: Applying source-code verification to a microkernel\u2014the VFiasco project. Technical report TUD-FI02-03-M\u00e4rz, TU Dresden (2002)","DOI":"10.1145\/1133373.1133405"},{"key":"9120_CR18","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1145\/360204.375719","volume-title":"Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2001). SIGPLAN Notices, vol. 36","author":"SS Ishtiaq","year":"2001","unstructured":"Ishtiaq, S.S., O\u2019Hearn, P.W.: BI as an assertion language for mutable data structures. In: Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2001). SIGPLAN Notices, vol. 36, pp. 14\u201326. ACM, New York (2001)"},{"key":"9120_CR19","volume-title":"The C Programming Language","author":"BW Kernighan","year":"1988","unstructured":"Kernighan, B.W., Ritchie, D.M.: The C Programming Language, 2nd edn. Prentice-Hall, Englewood Cliffs, New Jersey (1988)","edition":"2"},{"key":"9120_CR20","unstructured":"Klein, G.: Verified java bytecode verification. Ph.D. thesis, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen (2003)"},{"key":"9120_CR21","unstructured":"Kroening, D.: Application specific higher order logic theorem proving. In: Autexier, S., Mantel, H. (eds.) Proceedings of the 2nd Verification Workshop (VERIFY 2002), pp. 5\u201315, Technical Report no. 2002\/07. DIKU (2002)"},{"key":"9120_CR22","unstructured":"L4Ka Team. L4 eXperimental kernel reference manual version X.2. University of Karlsruhe. http:\/\/l4ka.org\/projects\/version4\/l4-x2.pdf (2001). Oct 2001"},{"issue":"1","key":"9120_CR23","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s10817-008-9099-0","volume":"41","author":"X Leroy","year":"2008","unstructured":"Leroy, X., Blazy, S.: Formal verification of a C-like memory model and its uses for verifying program transformations. J. Autom. Reason. 41(1), 1\u201331 (2008)","journal-title":"J. Autom. Reason."},{"key":"9120_CR24","first-page":"267","volume-title":"Proceedings of the Fifteenth ACM Symposium on Operating System Principles (SOSP 95). Operating System Review, vol. 29","author":"J Liedtke","year":"1995","unstructured":"Liedtke, J.: On \u03bc-kernel construction. In: Proceedings of the Fifteenth ACM Symposium on Operating System Principles (SOSP 95). Operating System Review, vol. 29, pp. 267\u2013284. ACM, New York (1995)"},{"key":"9120_CR25","doi-asserted-by":"crossref","unstructured":"Marti, N., Affeldt, R., Yonezawa, A.: Verification of the heap manager of an operating system using separation logic. In: Third workshop on Semantics, Program Analysis, and Computing Environments For Memory Management (SPACE 2006), pp. 61\u201372. Charleston, South Carolina (2006)","DOI":"10.1007\/11901433_22"},{"issue":"1\u20132","key":"9120_CR26","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1016\/j.ic.2004.10.007","volume":"199","author":"F Mehta","year":"2005","unstructured":"Mehta, F., Nipkow, T.: Proving pointer programs in higher-order logic. Inf. Comput. 199(1\u20132), 200\u2013227 (2005)","journal-title":"Inf. Comput."},{"key":"9120_CR27","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1145\/378795.378851","volume-title":"Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation. SIGPLAN Notices, vol. 37","author":"A M\u00f8ller","year":"2001","unstructured":"M\u00f8ller, A., Schwartzbach, M.I.: The pointer assertion logic engine. In: Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation. SIGPLAN Notices, vol. 37, pp. 221\u2013231. ACM, New York (2001)"},{"key":"9120_CR28","doi-asserted-by":"crossref","unstructured":"Morris, J.M.: A general axiom of assignment. In: Broy, M., Schmidt, G. (eds.) Theoretical Foundations of Programming Methodology (Proceedings of the 1981 Maktoberdorf Summer School), pp. 25\u201351 (1982)","DOI":"10.1007\/978-94-009-7893-5_3"},{"key":"9120_CR29","unstructured":"Moy, Y.: Union and cast in deductive verification. In: C\/C++ Verification Workshop, pp. 1\u201316. Technical report ICIS-R07015. Radboud University Nijmegen (2007)"},{"key":"9120_CR30","first-page":"213","volume-title":"Proceedings of the 11th International Conference on Compiler Construction (CC 2002). Lecture Notes in Computer Science, vol. 2304","author":"GC Necula","year":"2002","unstructured":"Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: Intermediate language and tools for analysis and transformation of C programs. In: Horspool, R.N. (eds.) Proceedings of the 11th International Conference on Compiler Construction (CC 2002). Lecture Notes in Computer Science, vol. 2304, pp. 213\u2013228. Springer, New York (2002)"},{"issue":"4","key":"9120_CR31","doi-asserted-by":"crossref","first-page":"320","DOI":"10.1007\/BF01887212","volume":"1","author":"T Nipkow","year":"1989","unstructured":"Nipkow, T.: Term rewriting and beyond\u2014theorem proving in Isabelle. Form. Asp. Comput. 1(4), 320\u2013338 (1989)","journal-title":"Form. Asp. Comput."},{"key":"9120_CR32","unstructured":"Norrish, M.: C formalised in HOL. Ph.D. thesis, Computer Laboratory, University of Cambridge (1998)"},{"key":"9120_CR33","first-page":"1","volume-title":"Proceedings of the 15th International Workshop on Computer Science Logic (CSL 2001). Lecture Notes in Computer Science, vol. 2142","author":"PW O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) Proceedings of the 15th International Workshop on Computer Science Logic (CSL 2001). Lecture Notes in Computer Science, vol. 2142, pages 1\u201319. Springer, New York (2001)"},{"key":"9120_CR34","first-page":"225","volume-title":"Proceedings of the 9th European Symposium on Research in Computer Security (ESORICS 2004). Lecture Notes in Computer Science, vol. 3193","author":"Oheimb","year":"2004","unstructured":"Oheimb: D.v.: Information flow control revisited: noninfluence = noninterference + nonleakage. In: Samarati, P., Ryan, P.Y.A., Gollmann, D., Molva, R. (eds.) Proceedings of the 9th European Symposium on Research in Computer Security (ESORICS 2004). Lecture Notes in Computer Science, vol. 3193, pages 225\u2013243. Springer, New York (2004)"},{"issue":"3","key":"9120_CR35","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/BF00248324","volume":"5","author":"LC Paulson","year":"1989","unstructured":"Paulson, L.C.: The foundation of a generic theorem prover. J. Autom. Reason. 5(3), 363\u2013397 (1989)","journal-title":"J. Autom. Reason."},{"key":"9120_CR36","first-page":"508","volume-title":"Proceedings of the 14th International Symposium on Formal Methods. Lecture Notes in Computer Science, vol. 4085","author":"V Preoteasa","year":"2006","unstructured":"Preoteasa, V.: Mechanical verification of recursive procedures manipulating pointers using separation logic. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) Proceedings of the 14th International Symposium on Formal Methods. Lecture Notes in Computer Science, vol. 4085, pp. 508\u2013523. Springer, New York (2006)"},{"key":"9120_CR37","first-page":"303","volume-title":"Millenial Perspectives in Computer Science","author":"JC Reynolds","year":"2000","unstructured":"Reynolds, J.C.: Intuitionistic reasoning about shared mutable data structures. In: Davies, J., Roscoe, B., Woodcock, J. (eds.) Millenial Perspectives in Computer Science, pp. 303\u2013321. Palgrave, Houndsmill, Hampshire (2000)"},{"key":"9120_CR38","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS 2002), pp. 55\u201374. IEEE Computer Society (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"9120_CR39","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/154766.155580","volume-title":"Proceedings of the ACM History of Programming Languages Conference (HOPL-II). SIGPLAN Notices, vol. 28","author":"DM Ritchie","year":"1993","unstructured":"Ritchie, D.M.: The development of the C language. In: Proceedings of the ACM History of Programming Languages Conference (HOPL-II). SIGPLAN Notices, vol. 28, pp. 201\u2013208. ACM, New York (1993)"},{"key":"9120_CR40","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1145\/292540.292552","volume-title":"Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1999)","author":"M Sagiv","year":"1999","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. In: Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1999), pp. 105\u2013118. ACM, New York (1999)"},{"key":"9120_CR41","doi-asserted-by":"crossref","unstructured":"Schirmer, N.: Verification of sequential imperative programs in Isabelle\/HOL. Ph.D. thesis, Technische Universit\u00e4t M\u00fcnchen (2006)","DOI":"10.1007\/978-3-540-32275-7_26"},{"key":"9120_CR42","first-page":"65","volume-title":"Proceedings of the IEEE\/NASA Workshop Leveraging Applications of Formal Methods, Verification, and Validation (IEEE\/NASA ISoLA 2005)","author":"B Schlich","year":"2005","unstructured":"Schlich, B., Kowalewski, S.: Model checking C source code for embedded systems. In: Margaria, T., Steffen, B., Hinchey, M.G. (eds.) Proceedings of the IEEE\/NASA Workshop Leveraging Applications of Formal Methods, Verification, and Validation (IEEE\/NASA ISoLA 2005), pp. 65\u201377. NASA, Maryland, USA (2005). NASA\/CP-2005-212788"},{"key":"9120_CR43","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1145\/1215995.1216004","volume-title":"Proceedings of the 3rd Workshop on Programming Languages and Operating Systems: Linguistic Support for Modern Operating Systems (PLOS 2006)","author":"J Shapiro","year":"2006","unstructured":"Shapiro, J.: Programming language challenges in systems codes: why systems programmers still use C, and what to do about it. In: Probst, C.W. (ed.) Proceedings of the 3rd Workshop on Programming Languages and Operating Systems: Linguistic Support for Modern Operating Systems (PLOS 2006), pp. 9. ACM, New York (2006)"},{"key":"9120_CR44","unstructured":"System Architecture Group. The L4Ka::Pistachio microkernel. White paper, University of Karlsruhe, May 2003. http:\/\/l4ka.org\/projects\/pistachio\/pistachio-whitepaper.pdf"},{"key":"9120_CR45","unstructured":"Tews, H.: Verifying Duff\u2019s device: a simple compositional denotational semantics for goto and computed jumps (2004). http:\/\/www.cs.ru.nl\/~tews\/Goto\/goto.pdf"},{"key":"9120_CR46","unstructured":"Tuch, H.: Formal memory models for verifying C systems code. Ph.D. thesis, University of NSW (2008)"},{"key":"9120_CR47","first-page":"97","volume-title":"Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2007)","author":"H Tuch","year":"2007","unstructured":"Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: Hofmann, M., Felleisen, M. (eds.) Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2007), pp. 97\u2013108. ACM, New York (2007)"},{"key":"9120_CR48","first-page":"250","volume-title":"Proceedings of the 18th International Workshop on Computer Science Logic (CSL 2004). Lecture Notes in Computer Science, vol. 3210","author":"T Weber","year":"2004","unstructured":"Weber, T.: Towards mechanized program verification with separation logic. In: Marcinkowski, J., Tarlecki, A. (eds.) Proceedings of the 18th International Workshop on Computer Science Logic (CSL 2004). Lecture Notes in Computer Science, vol. 3210, pp. 250\u2013264. Springer, New York (2004)"},{"key":"9120_CR49","first-page":"307","volume-title":"Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 97). Lecture Notes in Computer Science, vol. 1275","author":"M Wenzel","year":"1997","unstructured":"Wenzel, M.: Type classes and overloading in higher-order logic. In: Gunter, E.L., Felty, A.P. (eds.) Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 97). Lecture Notes in Computer Science, vol. 1275, pp. 307\u2013322. Springer, New York (1997)"},{"key":"9120_CR50","first-page":"402","volume-title":"Proceedings of the 5th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2002). Lecture Notes in Computer Science, vol. 2303","author":"H Yang","year":"2002","unstructured":"Yang, H., O\u2019Hearn, P.W.: A semantic basis for local reasoning. In: Nielsen, M., Engberg, U. (eds.) Proceedings of the 5th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2002). Lecture Notes in Computer Science, vol. 2303, pp. 402\u2013416. Springer, New York (2002)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-009-9120-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-009-9120-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-009-9120-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,24]],"date-time":"2023-05-24T18:17:19Z","timestamp":1684952239000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-009-9120-2"}},"subtitle":["Structured Types, Separation Logic and Theorem Proving"],"short-title":[],"issued":{"date-parts":[[2009,4]]},"references-count":50,"journal-issue":{"issue":"2-4","published-print":{"date-parts":[[2009,4]]}},"alternative-id":["9120"],"URL":"https:\/\/doi.org\/10.1007\/s10817-009-9120-2","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,4]]}}}