{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T06:52:12Z","timestamp":1773557532305,"version":"3.50.1"},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"1-4","license":[{"start":{"date-parts":[[2018,2,21]],"date-time":"2018-02-21T00:00:00Z","timestamp":1519171200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2018,2,21]],"date-time":"2018-02-21T00:00:00Z","timestamp":1519171200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100000083","name":"Directorate for Computer and Information Science and Engineering","doi-asserted-by":"publisher","award":["CCF-1521602"],"award-info":[{"award-number":["CCF-1521602"]}],"id":[{"id":"10.13039\/100000083","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"crossref","award":["FA8750-12-2-0293"],"award-info":[{"award-number":["FA8750-12-2-0293"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2018,6]]},"DOI":"10.1007\/s10817-018-9457-5","type":"journal-article","created":{"date-parts":[[2018,2,21]],"date-time":"2018-02-21T05:17:57Z","timestamp":1519190277000},"page":"367-422","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":84,"title":["VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs"],"prefix":"10.1007","volume":"61","author":[{"given":"Qinxiang","family":"Cao","sequence":"first","affiliation":[]},{"given":"Lennart","family":"Beringer","sequence":"additional","affiliation":[]},{"given":"Samuel","family":"Gruetter","sequence":"additional","affiliation":[]},{"given":"Josiah","family":"Dodds","sequence":"additional","affiliation":[]},{"given":"Andrew W.","family":"Appel","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,2,21]]},"reference":[{"key":"9457_CR1","doi-asserted-by":"crossref","unstructured":"Affeldt, R., Marti, N.: Towards formal verification of TLS network packet processing written in C. In: Might, M., Van Horn, D., Abel, A., Sheard, T. (eds.) Proceedings of the 7th Workshop on Programming Languages Meets Program Verification, pp. 35\u201346. ACM (2013)","DOI":"10.1145\/2428116.2428124"},{"issue":"2","key":"9457_CR2","doi-asserted-by":"publisher","first-page":"7:1","DOI":"10.1145\/2701415","volume":"37","author":"AW Appel","year":"2015","unstructured":"Appel, A.W.: Verification of a cryptographic primitive: SHA-256. ACM Trans. Program. Lang. Syst. 37(2), 7:1\u20137:31 (2015)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9457_CR3","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107256552","volume-title":"Program Logics for Certified Compilers","author":"AW Appel","year":"2014","unstructured":"Appel, A.W., Dockins, R., Hobor, A., Beringer, L., Dodds, J., Stewart, G., Blazy, S., Leroy, X.: Program Logics for Certified Compilers. Cambridge University Press, Cambridge (2014)"},{"issue":"5","key":"9457_CR4","doi-asserted-by":"publisher","first-page":"657","DOI":"10.1145\/504709.504712","volume":"23","author":"AW Appel","year":"2001","unstructured":"Appel, A.W., McAllester, D.: An indexed model of recursive types for foundational proof-carrying code. ACM Trans. Program. Lang. Syst. 23(5), 657\u2013683 (2001)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9457_CR5","doi-asserted-by":"crossref","unstructured":"Bengtson, J., Jensen, J.B., Birkedal, L.: Charge! a framework for higher-order separation logic in Coq. In: ITP, pp. 315\u2013331 (2012)","DOI":"10.1007\/978-3-642-32347-8_21"},{"key":"9457_CR6","doi-asserted-by":"crossref","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Symbolic execution with separation logic. In: Yi, K. (ed.) Programming Languages and Systems, Third Asian Symposium, APLAS 2005, Tsukuba, Japan, November 2\u20135, 2005, Proceedings, Volume 3780 of Lecture Notes in Computer Science, pp. 52\u201368. Springer (2005)","DOI":"10.1007\/11575467_5"},{"key":"9457_CR7","unstructured":"Beringer, L., Petcher, A., Ye, K.Q., Appel, A.W.: Verified correctness and security of OpenSSL HMAC. In: 24th USENIX Security Symposium, pp. 207\u2013221. USENIX Assocation (2015)"},{"key":"9457_CR8","doi-asserted-by":"crossref","unstructured":"Bernstein, D.J., van Gastel, B., Janssen, W., Lange, T., Schwabe, P., Smetsers, S.: Tweetnacl: a crypto library in 100 tweets. In: Aranha, D.F., Menezes, A. (eds.) Progress in Cryptology\u2014LATINCRYPT 2014\u2014Third International Conference on Cryptology and Information Security in Latin America, Florian\u00f3polis, Brazil, September 17\u201319, 2014, Revised Selected Papers, Volume 8895 of Lecture Notes in Computer Science, pp. 64\u201383. Springer (2014)","DOI":"10.1007\/978-3-319-16295-9_4"},{"key":"9457_CR9","doi-asserted-by":"publisher","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. SIGPLAN Not. 44, 289\u2013300 (2009)","journal-title":"SIGPLAN Not."},{"issue":"9","key":"9457_CR10","doi-asserted-by":"publisher","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":"9457_CR11","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: The Bedrock structured programming system: combining generative metaprogramming and Hoare logic in an extensible program verifier. In: ICFP\u201913: Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming (2013)","DOI":"10.1145\/2500365.2500592"},{"key":"9457_CR12","unstructured":"Clarke, E.M., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In Jensen, K., Podelski, A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29\u2013April 2, 2004, Proceedings, Volume 2988 of Lecture Notes in Computer Science, pp. 168\u2013176. Springer (2004)"},{"key":"9457_CR13","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Proceedings of Symposium in Applied Mathematics, pp. 19\u201332. Providence, Rhode Island (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"9457_CR14","unstructured":"Gruetter, S.: Improving the Coq proof automation tactics of the Verified Software Toolchain, based on a case study on verifying a C implementation of the AES encryption algorithm. Master thesis. Ecole Polytechnique F\u00e9d\u00e9rale de Lausanne (2017)"},{"key":"9457_CR15","doi-asserted-by":"crossref","unstructured":"Gu\u00e9neau, A., Myreen, M.O., Kumar, R., Norrish, M.: Verified characteristic formulae for CakeML. In: Programming Languages and Systems: 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22\u201329, 2017, Proceedings, pp. 584\u2013610. Springer, Berlin (2017)","DOI":"10.1007\/978-3-662-54434-1_22"},{"issue":"10","key":"9457_CR16","doi-asserted-by":"publisher","first-page":"578","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 578\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"9457_CR17","doi-asserted-by":"crossref","unstructured":"Hobor, A., Dockins, R., Appel, A.W.: A theory of indirection via approximation. In: Proceedings of the 37th Annual ACM Symposium on Principles of Programming Languages (POPL\u201910), pp. 171\u2013185 (2010)","DOI":"10.1145\/1706299.1706322"},{"key":"9457_CR18","unstructured":"Hobor, A., Villard, J.: The ramifications of sharing in data structures. In: Giacobazzi, R., Cousot, R. (eds.) The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201913, Rome, Italy, January 23\u201325, 2013, pp. 523\u2013536. ACM (2013)"},{"key":"9457_CR19","doi-asserted-by":"crossref","unstructured":"Jung, R., Swasey, D., Sieczkowski, F., Svendsen, K., Turon, A., Birkedal, L., Dreyer, D.: Iris: monoids and invariants as an orthogonal basis for concurrent reasoning. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2015)","DOI":"10.1145\/2676726.2676980"},{"key":"9457_CR20","unstructured":"Kleymann, T.: Hoare logic and VDM: machine-checked soundness and completeness proofs. PhD thesis, University of Edinburgh, UK (1998)"},{"key":"9457_CR21","unstructured":"Krebbers, R.: The C standard formalized in Coq. PhD thesis, Radboud University (2015)"},{"key":"9457_CR22","doi-asserted-by":"crossref","unstructured":"Krebbers, R., Jung, R., Bizjak, A., Jourdan, J.-H., Dreyer, D., Birkedal, L.: The essence of higher-order concurrent separation logic. In: European Symposium on Programming, pp. 696\u2013723. Springer (2017)","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"9457_CR23","unstructured":"Krebbers, R., Timany, A., Birkedal, L.: Interactive proofs in higher-order concurrent separation logic. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18\u201320, 2017, pp. 205\u2013217. ACM (2017)"},{"key":"9457_CR24","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning\u201416th International Conference, LPAR-16, Dakar, Senegal, April 25\u2013May 1, 2010, Revised Selected Papers, Volume 6355 of Lecture Notes in Computer Science, pp. 348\u2013370. Springer (2010)","DOI":"10.1007\/978-3-642-17511-4_20"},{"issue":"7","key":"9457_CR25","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"key":"9457_CR26","doi-asserted-by":"crossref","unstructured":"Mansky, W., Appel, A.W., Nogin, A.: A verified messaging system. In: Proceedings of the 2017 ACM International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA \u201917. ACM (2017)","DOI":"10.1145\/3133911"},{"key":"9457_CR27","unstructured":"Matthews, J., Moore, J.S., Ray, S., Vroon, D.: Verification condition generation via theorem proving. In: Hermann, M., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference, LPAR 2006, Phnom Penh, Cambodia, November 13\u201317, 2006, Proceedings, Volume 4246 of Lecture Notes in Computer Science, pp. 362\u2013376. Springer (2006)"},{"key":"9457_CR28","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Hoare logics for recursive procedures and unbounded nondeterminism. In: Bradfield, J.C. (ed.) Computer Science Logic, 16th International Workshop, CSL 2002, 11th Annual Conference of the EACSL, Edinburgh, Scotland, UK, September 22\u201325, 2002, Proceedings, Volume 2471 of Lecture Notes in Computer Science, pp. 103\u2013119. Springer (2002)","DOI":"10.1007\/3-540-45793-3_8"},{"key":"9457_CR29","doi-asserted-by":"crossref","unstructured":"Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: LICS 2002: IEEE Symposium on Logic in Computer Science, pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"9457_CR30","unstructured":"Signoles, J.: Foncteurs imp\u00e9ratifs et compos\u00e9s: la notion de projets dans Frama-C. In: Schmitt, A. (ed.) JFLA 2009, Vingti\u00e8mes Journ\u00e9es Francophones des Langages Applicatifs, Saint Quentin sur Is\u00e8re, France, January 31\u2013February 3, 2009. Proceedings, Volume 7.2 of Studia Informatica Universalis, pp. 245\u2013280 (2009)"},{"key":"9457_CR31","unstructured":"Wildmoser, M.: Verified proof carrying code. PhD thesis, Technical University Munich (2005)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-018-9457-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9457-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9457-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,1]],"date-time":"2025-07-01T22:51:32Z","timestamp":1751410292000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-018-9457-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,2,21]]},"references-count":31,"journal-issue":{"issue":"1-4","published-print":{"date-parts":[[2018,6]]}},"alternative-id":["9457"],"URL":"https:\/\/doi.org\/10.1007\/s10817-018-9457-5","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,2,21]]},"assertion":[{"value":"1 April 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 January 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 February 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}