{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T16:02:32Z","timestamp":1781193752455,"version":"3.54.1"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032280787","type":"print"},{"value":"9783032280794","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-28079-4_22","type":"book-chapter","created":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T15:33:17Z","timestamp":1781191997000},"page":"477-484","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Foundational VeriFast: Pragmatic Certification of\u00a0Verification Tool Results Through Hinted Mirroring"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3605-249X","authenticated-orcid":false,"given":"Bart","family":"Jacobs","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,6,12]]},"reference":[{"key":"22_CR1","doi-asserted-by":"crossref","unstructured":"Appel, A.W.: Verified software toolchain. In: Proceedings of the 20th European Conference on Programming Languages and Systems: Part of the Joint European Conferences on Theory and Practice of Software, ESOP 2011\/ETAPS 2011, pp. 1\u201317. Springer, Heidelberg (2011)","DOI":"10.1007\/978-3-642-19718-5_1"},{"key":"22_CR2","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-25379-9_12","volume-title":"Certified Programs and Proofs","author":"M Armand","year":"2011","unstructured":"Armand, M., Faure, G., Gr\u00e9goire, B., Keller, C., Th\u00e9ry, L., Werner, B.: A modular integration of SAT\/SMT solvers to Coq through proof witnesses. In: Jouannaud, J.P., Shao, Z. (eds.) Certified Programs and Proofs, pp. 135\u2013150. Springer, Berlin Heidelberg, Berlin, Heidelberg (2011)"},{"key":"22_CR3","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-642-22438-6_11","volume-title":"Automated Deduction - CADE-23","author":"JC Blanchette","year":"2011","unstructured":"Blanchette, J.C., B\u00f6hme, S., Paulson, L.C.: Extending Sledgehammer with SMT solvers. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) Automated Deduction - CADE-23, pp. 116\u2013130. Springer, Heidelberg (2011)"},{"key":"22_CR4","doi-asserted-by":"publisher","unstructured":"Cohen, J.M., Johnson-Freyd, P.: A formalization of core Why3 in Coq. Proc. ACM Program. Lang. 8(POPL) (2024). https:\/\/doi.org\/10.1145\/3632902","DOI":"10.1145\/3632902"},{"key":"22_CR5","doi-asserted-by":"publisher","unstructured":"Dardinier, T., Sammler, M., Parthasarathy, G., Summers, A.J., M\u00fcller, P.: Formal foundations for translational separation logic verifiers. Proc. ACM Program. Lang. 9(POPL) (Jan 2025). https:\/\/doi.org\/10.1145\/3704856","DOI":"10.1145\/3704856"},{"key":"22_CR6","doi-asserted-by":"publisher","unstructured":"G\u00e4her, L., Sammler, M., Jung, R., Krebbers, R., Dreyer, D.: RefinedRust: a type system for high-assurance verification of Rust programs. Proc. ACM Program. Lang. 8(PLDI) (2024). https:\/\/doi.org\/10.1145\/3656422","DOI":"10.1145\/3656422"},{"key":"22_CR7","doi-asserted-by":"publisher","unstructured":"Jacobs, B.: VeriFast 26, 01 (2026). https:\/\/doi.org\/10.5281\/zenodo.19415099","DOI":"10.5281\/zenodo.19415099"},{"key":"22_CR8","doi-asserted-by":"publisher","unstructured":"Jacobs, B., Vogels, F., Piessens, F.: Featherweight VeriFast. Logical Methods Comput. Sci. 11(3), 19 (2015). https:\/\/doi.org\/10.2168\/LMCS-11(3:19)2015, https:\/\/lmcs.episciences.org\/1595","DOI":"10.2168\/LMCS-11(3:19)2015"},{"key":"22_CR9","doi-asserted-by":"publisher","unstructured":"Jung, R., Jourdan, J.H., Krebbers, R., Dreyer, D.: RustBelt: securing the foundations of the rust programming language. Proc. ACM Program. Lang. 2(POPL) (2017). https:\/\/doi.org\/10.1145\/3158154","DOI":"10.1145\/3158154"},{"key":"22_CR10","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151","volume":"28","author":"R Jung","year":"2018","unstructured":"Jung, R., Krebbers, R., Jourdan, J.H., Bizjak, A., Birkedal, L., Dreyer, D.: Iris from the ground up: a modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28, e20 (2018). https:\/\/doi.org\/10.1017\/S0956796818000151","journal-title":"J. Funct. Program."},{"key":"22_CR11","unstructured":"Jung, R., et al.: MiniRust (2025). https:\/\/github.com\/minirust\/minirust"},{"key":"22_CR12","doi-asserted-by":"crossref","unstructured":"Leroy, X.: A formally verified compiler back-end. J. Autom. Reasoning 43(4), 363\u2013446 (2009). http:\/\/xavierleroy.org\/publi\/compcert-backend.pdf","DOI":"10.1007\/s10817-009-9155-4"},{"key":"22_CR13","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Proceedings of the 15th International Workshop on Computer Science Logic, CSL 2001, pp. 1\u201319. Springer, Heidelberg (2001)","DOI":"10.1007\/3-540-44802-0_1"},{"key":"22_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"704","DOI":"10.1007\/978-3-030-81688-9_33","volume-title":"Computer Aided Verification","author":"G Parthasarathy","year":"2021","unstructured":"Parthasarathy, G., M\u00fcller, P., Summers, A.J.: Formally validating a practical verification condition generator. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 704\u2013727. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_33"},{"key":"22_CR15","doi-asserted-by":"publisher","unstructured":"Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, pp. 55\u201374 (2002). https:\/\/doi.org\/10.1109\/LICS.2002.1029817","DOI":"10.1109\/LICS.2002.1029817"},{"key":"22_CR16","doi-asserted-by":"publisher","unstructured":"Sammler, M., Lepigre, R., Krebbers, R., Memarian, K., Dreyer, D., Garg, D.: RefinedC: automating the foundational verification of C code with refined ownership types. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021, pp. 158\u2013174. ACM, New York, NY, USA (2021). https:\/\/doi.org\/10.1145\/3453483.3454036","DOI":"10.1145\/3453483.3454036"},{"key":"22_CR17","doi-asserted-by":"publisher","unstructured":"The Coq Development Team: The Coq proof assistant (2024). https:\/\/doi.org\/10.5281\/zenodo.14542673","DOI":"10.5281\/zenodo.14542673"},{"key":"22_CR18","doi-asserted-by":"publisher","unstructured":"Zhou, L., Qin, J., Wang, Q., Appel, A.W., Cao, Q.: VST-A: a foundationally sound annotation verifier. Proc. ACM Program. Lang. 8(POPL) (2024). https:\/\/doi.org\/10.1145\/3632911","DOI":"10.1145\/3632911"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-28079-4_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T15:33:18Z","timestamp":1781191998000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-28079-4_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032280787","9783032280794"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-28079-4_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"12 June 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"None.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Los Angeles, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/nfm2026.github.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}