{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,15]],"date-time":"2025-05-15T09:40:02Z","timestamp":1747302002275,"version":"3.40.5"},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2014,12,24]],"date-time":"2014-12-24T00:00:00Z","timestamp":1419379200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2015,3]]},"DOI":"10.1007\/s10817-014-9319-8","type":"journal-article","created":{"date-parts":[[2014,12,23]],"date-time":"2014-12-23T22:16:06Z","timestamp":1419372966000},"page":"199-284","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Symbolic Execution Proofs for Higher Order Store Programs"],"prefix":"10.1007","volume":"54","author":[{"given":"Bernhard","family":"Reus","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nathaniel","family":"Charlton","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ben","family":"Horsfall","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,12,24]]},"reference":[{"key":"9319_CR1","unstructured":"The Crowfoot website. www.sussex.ac.uk\/informatics\/crowfoot (2011)"},{"key":"9319_CR2","doi-asserted-by":"crossref","unstructured":"Beckmann, O., Houghton, A., Mellor, M.R., Kelly, P.H.J.: Runtime code generation in C++ as a foundation for domain-specific optimisation. In: Domain-Specific Program Generation, pp 291\u2013306 (2003)","DOI":"10.1007\/978-3-540-25935-0_17"},{"key":"9319_CR3","doi-asserted-by":"crossref","unstructured":"Benton, N., Kennedy, A., Beringer, L., Hofmann, M.: Relational semantics for effect-based program transformations: higher-order store. In: PPDP, pp 301\u2013312 (2009)","DOI":"10.1145\/1599410.1599447"},{"key":"9319_CR4","doi-asserted-by":"crossref","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Smallfoot: Modular automatic assertion checking with separation logic. In: FMCO, pp 115\u2013137 (2005)","DOI":"10.1007\/11804192_6"},{"key":"9319_CR5","doi-asserted-by":"crossref","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Symbolic execution with separation logic. In: APLAS, pp 52\u201368 (2005)","DOI":"10.1007\/11575467_5"},{"key":"9319_CR6","doi-asserted-by":"crossref","unstructured":"Biering, B., Birkedal, L., Torp-Smith, N. : Bi-hyperdoctrines, higher-order separation logic, and abstraction. ACM Trans. Program. Lang. Syst. 29 (5) (2007)","DOI":"10.1145\/1275497.1275499"},{"key":"9319_CR7","doi-asserted-by":"crossref","unstructured":"Birkedal, L., Reus, B., Schwinghammer, J., St\u00f8vring, K., Thamsborg, J., Yang, H.: Step-indexed Kripke models over recursive worlds. In: POPL\u201911, pp 119\u2013132. IEEE (2011)","DOI":"10.1145\/1926385.1926401"},{"key":"9319_CR8","doi-asserted-by":"crossref","unstructured":"Birkedal, L., Torp-Smith, N., Yang, H.: Semantics of separation-logic typing and higher-order frame rules for Algol-like languages. LMCS 2 (5) (2006)","DOI":"10.2168\/LMCS-2(5:1)2006"},{"key":"9319_CR9","unstructured":"Blom, S., Huisman, M.: Witnessing the elimination of magic wands (2013)"},{"key":"9319_CR10","doi-asserted-by":"crossref","unstructured":"Cai, H., Shao, Z., Vaynberg, A.: Certified self-modifying code. In: PLDI, pp 66\u201377 (2007)","DOI":"10.1145\/1273442.1250743"},{"issue":"1","key":"9319_CR11","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1145\/1594834.1480917","volume":"44","author":"C Calcagno","year":"2009","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. ACM SIGPLAN Notices 44 (1), 289\u2013300 (2009)","journal-title":"ACM SIGPLAN Notices"},{"key":"9319_CR12","doi-asserted-by":"crossref","unstructured":"Chargu\u00e9raud, A: Characteristic formulae for the verification of imperative programs. In: Chakravarty, M.M.T., Hu, Z., Danvy, O. (eds.) ICFP, pp 418\u2013430. ACM (2011)","DOI":"10.1145\/2034574.2034828"},{"key":"9319_CR13","doi-asserted-by":"crossref","unstructured":"Charlton, N., Horsfall, B., Reus, B.: Formal reasoning about runtime code update. In: Abiteboul, S., B\u00f6hm, K., Koch, C., Tan, K.-L. (eds.) ICDE Workshops, pp 134\u2013138. IEEE (2011)","DOI":"10.1109\/ICDEW.2011.5767624"},{"key":"9319_CR14","doi-asserted-by":"crossref","unstructured":"Charlton, N., Horsfall, B., Reus, B. : Crowfoot: A verifier for higher-order store programs. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI, volume 7148 of Lecture Notes in Computer Science, pp 136\u2013151. Springer (2012)","DOI":"10.1007\/978-3-642-27940-9_10"},{"key":"9319_CR15","unstructured":"Charlton, N., Reus, B.: A deeper understanding of the deep frame axiom. Extended abstract, presented at LOLA (Syntax and Semantics of Low Level Languages) (2010)"},{"key":"9319_CR16","doi-asserted-by":"crossref","unstructured":"Charlton, N., Reus, B.: Specification patterns and proofs for recursion through the store. In: FCT, pp 310\u2013321 (2011)","DOI":"10.1007\/978-3-642-22953-4_27"},{"issue":"9","key":"9319_CR17","doi-asserted-by":"crossref","first-page":"1006","DOI":"10.1016\/j.scico.2010.07.004","volume":"77","author":"W-N Chin","year":"2012","unstructured":"Chin, W.-N., David, C., Nguyen, H.H., Qin, S.: Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Sci. Comput. Program. 77 (9), 1006\u20131036 (2012)","journal-title":"Sci. Comput. Program."},{"key":"9319_CR18","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: Mostly-automated verification of low-level programs in computational separation logic. In: Hall, M.W., Padua, D.A. (eds.) PLDI, pp 234\u2013245. ACM (2011)","DOI":"10.1145\/1993316.1993526"},{"key":"9319_CR19","doi-asserted-by":"crossref","unstructured":"Chlipala, A., Malecha, J.G., Morrisett, G., Shinnar, A., Wisnesky, R.: Effective interactive proofs for higher-order imperative programs. In: Hutton, G., Tolmach, A.P. (eds.) ICFP, pp 79\u201390. ACM (2009)","DOI":"10.1145\/1596550.1596565"},{"key":"9319_CR20","doi-asserted-by":"crossref","unstructured":"Distefano, D., O\u2019Hearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: TACAS, pp 287\u2013302 (2006)","DOI":"10.1007\/11691372_19"},{"key":"9319_CR21","doi-asserted-by":"crossref","unstructured":"Distefano, D., Parkinson, M.J.: jStar: towards practical verification for Java. In: OOPSLA, pp 213\u2013226 (2008)","DOI":"10.1145\/1449955.1449782"},{"key":"9319_CR22","doi-asserted-by":"crossref","unstructured":"Gherghina, C., David, C., Qin, S., Chin, W.-N.: Structured specifications for better verification of heap-manipulating programs. In: FM, pp 386\u2013401 (2011)","DOI":"10.1007\/978-3-642-21437-0_29"},{"key":"9319_CR23","doi-asserted-by":"crossref","unstructured":"Gordon, M.J.C., Milner, R., Wadsworth, C.P.: Edinburgh LCF, volume 78 of Lecture Notes in Computer Science. Springer (1979)","DOI":"10.1007\/3-540-09724-4"},{"key":"9319_CR24","unstructured":"Henderson, B.: Linux loadable kernel module HOWTO (v1.09). Available online http:\/\/tldp.org\/HOWTO\/Module-HOWTO\/ (2006)"},{"key":"9319_CR25","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1007\/BFb0059696","volume-title":"Symposium on Semantics of Algorithmic Languages, volume 188 of Lecture Notes in Mathematics","author":"CAR Hoare","year":"1971","unstructured":"Hoare, C.A.R.: Procedures and parameters: An axiomatic approach. In: Engeler, E. (ed.) Symposium on Semantics of Algorithmic Languages, volume 188 of Lecture Notes in Mathematics, pp 102\u2013116. Springer Berlin, Heidelberg (1971)"},{"key":"9319_CR26","unstructured":"Honda, K., Yoshida, N., Berger, M.: An observationally complete program logic for imperative higher-order functions. In: LICS, pp 270\u2013279 (2005)"},{"key":"9319_CR27","unstructured":"Horsfall, B.: Automated reasoning for reflective programs. PhD thesis (2014)"},{"key":"9319_CR28","doi-asserted-by":"crossref","unstructured":"Horsfall, B., Charlton, N., Reus, B.: Verifying the reflective visitor pattern. In: FtFJP, pp 27\u201334 (2012)","DOI":"10.1145\/2318202.2318208"},{"key":"9319_CR29","doi-asserted-by":"crossref","unstructured":"Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: A powerful, sound, predictable, fast verifier for C and Java. In: NASA Formal Methods, pp 41\u201355 (2011)","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"9319_CR30","doi-asserted-by":"crossref","unstructured":"Jacobs, B, Smans, J, Piessens, F: A quick tour of the VeriFast program verifier. In: APLAS, pp 304\u2013311 (2010)","DOI":"10.1007\/978-3-642-17164-2_21"},{"key":"9319_CR31","unstructured":"Lee, W., Park, S.: A proof system for separation logic with magic wand. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL, pp. 477\u2013490, New York, USA, 2014. ACM"},{"issue":"5\u20136","key":"9319_CR32","doi-asserted-by":"crossref","first-page":"865","DOI":"10.1017\/S0956796808006953","volume":"18","author":"AJ Nanevski","year":"2008","unstructured":"Nanevski, A. J., Morrisett, G., Birkedal, L.: Hoare type theory, polymorphism and separation. J. Funct. Program. 18 (5\u20136), 865\u2013911 (2008)","journal-title":"J. Funct. Program."},{"key":"9319_CR33","doi-asserted-by":"crossref","unstructured":"Ni, Z., Shao, Z.: Certified assembly programming with embedded code pointers. In: POPL, pp 320\u2013333 (2006)","DOI":"10.1145\/1111320.1111066"},{"key":"9319_CR34","doi-asserted-by":"crossref","unstructured":"Pottier, F.: Hiding local state in direct style: a higher-order anti-frame rule. In LICS, pp. 331\u2013340, Pittsburgh, Pennsylvania (2008)","DOI":"10.1109\/LICS.2008.16"},{"issue":"1","key":"9319_CR35","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1016\/j.tcs.2003.11.020","volume":"315","author":"DJ Pym","year":"2004","unstructured":"Pym, D.J., O\u2019Hearn, P.W., Yang, H.: Possible worlds and resources: the semantics of BI. Theor. Comput. Sci. 315 (1), 257\u2013305 (2004)","journal-title":"Theor. Comput. Sci."},{"key":"9319_CR36","doi-asserted-by":"crossref","unstructured":"Reus, B., Schwinghammer, J.: Separation logic for higher-order store. In: CSL, pp 575\u2013590 (2006)","DOI":"10.1007\/11874683_38"},{"key":"9319_CR37","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS, pp 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"issue":"1\u20132","key":"9319_CR38","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1016\/S0304-3975(96)80711-0","volume":"170","author":"JJMM Rutten","year":"1996","unstructured":"Rutten, J.J.M.M.: Elements of generalized ultrametric domain theory. Theor. Comput. Sci. 170 (1\u20132), 349\u2013381 (1996)","journal-title":"Theor. Comput. Sci."},{"key":"9319_CR39","volume-title":"Lightweight support for magic wands in an automatic verifier","author":"M Schwerhoff","year":"2014","unstructured":"Schwerhoff, M., Summers, A.J.: Lightweight support for magic wands in an automatic verifier. Technical report, ETH Zurich (2014)"},{"key":"9319_CR40","doi-asserted-by":"crossref","unstructured":"Schwinghammer, J., Birkedal, L., Reus, B., Yang, H.: Nested Hoare triples and frame rules for higher-order store. In: CSL, pp 440\u2013454 (2009)","DOI":"10.1007\/978-3-642-04027-6_32"},{"key":"9319_CR41","doi-asserted-by":"crossref","unstructured":"Schwinghammer, J., Birkedal, L., Reus, B., Yang, H.: Nested Hoare triples and frame rule for higher-order store. Logical Methods Comput. Sci. 7 (3) (2011)","DOI":"10.2168\/LMCS-7(3:21)2011"},{"key":"9319_CR42","doi-asserted-by":"crossref","unstructured":"Schwinghammer, J., Yang, H., Birkedal, L., Pottier, F., Reus, B: A semantic foundation for hidden state. In: FOSSACS, pp 2\u201317 (2010)","DOI":"10.1007\/978-3-642-12032-9_2"},{"key":"9319_CR43","doi-asserted-by":"crossref","unstructured":"Stoyle, G., Hicks, M., Bierman, G., Sewell, P., Neamtiu, I.: Mutatis mutandis: Safe and predictable dynamic software updating. ACM Trans. Program. Lang. Syst. 29 (4) (2007)","DOI":"10.1145\/1255450.1255455"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-014-9319-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-014-9319-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-014-9319-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,15]],"date-time":"2025-05-15T09:21:09Z","timestamp":1747300869000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-014-9319-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,12,24]]},"references-count":43,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2015,3]]}},"alternative-id":["9319"],"URL":"https:\/\/doi.org\/10.1007\/s10817-014-9319-8","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2014,12,24]]}}}