{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:43:46Z","timestamp":1780994626389,"version":"3.54.1"},"reference-count":78,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2022,8,29]],"date-time":"2022-08-29T00:00:00Z","timestamp":1661731200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["101040088"],"award-info":[{"award-number":["101040088"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,8,29]]},"abstract":"<jats:p>Verifying soundness of symbolic execution-based program verifiers is a  \nsignificant challenge. This is especially true if the resulting tool needs to be  \nusable outside of the proof assistant, in which case we cannot rely on shallowly  \nembedded assertion logics and meta-programming. The tool needs to manipulate  \ndeeply embedded assertions, and it is crucial for efficiency to eagerly prune  \nunreachable paths and simplify intermediate assertions in a way that can be  \njustified towards the soundness proof. Only a few such tools exist in the  \nliterature, and their soundness proofs are intricate and hard to generalize or  \nreuse. We contribute a novel, systematic approach for the construction and  \nsoundness proof of such a symbolic execution-based verifier. We first implement  \na shallow verification condition generator as an object language interpreter in  \na specification monad, using an abstract interface featuring angelic and demonic  \nnondeterminism. Next, we build a symbolic executor by implementing a similar  \ninterpreter, in a symbolic specification monad. This symbolic monad lives in a  \nuniverse that is Kripke-indexed by variables in scope and a path condition.  \nFinally, we reduce the soundness of the symbolic execution to the soundness of  \nthe shallow execution by relating both executors using a Kripke logical  \nrelation. We report on the practical application of these techniques in  \nKatamaran, a tool for verifying security guarantees offered by instruction set  \narchitectures (ISAs). The tool is fully verified by combining our symbolic  \nexecution machinery with a soundness proof of the shallow verification  \nconditions against an axiomatized separation logic, and an Iris-based  \nimplementation of the axioms, proven sound against the operational semantics.  \nBased on our experience with Katamaran, we can report good results on  \npracticality and efficiency of the tool, demonstrating practical viability of  \nour symbolic execution approach.<\/jats:p>","DOI":"10.1145\/3547628","type":"journal-article","created":{"date-parts":[[2022,8,31]],"date-time":"2022-08-31T19:39:26Z","timestamp":1661974766000},"page":"194-224","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Verified symbolic execution with Kripke specification monads (and no meta-programming)"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6411-438X","authenticated-orcid":false,"given":"Steven","family":"Keuchel","sequence":"first","affiliation":[{"name":"Vrije Universiteit Brussel, Belgium"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2878-7429","authenticated-orcid":false,"given":"Sander","family":"Huyghebaert","sequence":"additional","affiliation":[{"name":"Vrije Universiteit Brussel, Belgium"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3065-4980","authenticated-orcid":false,"given":"Georgy","family":"Lukyanov","sequence":"additional","affiliation":[{"name":"Newcastle University, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3862-6856","authenticated-orcid":false,"given":"Dominique","family":"Devriese","sequence":"additional","affiliation":[{"name":"KU Leuven, Belgium"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,8,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000186"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009878"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-12154-3_4"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-35672-3_1"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48168-0_32"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25379-9_18"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290384"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50010-2"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158104"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1674-2"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3182657"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1015761529444"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.6092\/issn.1972-5787\/4552"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9219-0"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30538-5_9"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_6"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_5"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107050884"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014565"},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201908)","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar , Daniel Dunbar , and Dawson Engler . 2008 . KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs . In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201908) . USENIX Association, 209\u2013224. http:\/\/www.usenix.org\/events\/osdi08\/tech\/full_papers\/cadar\/cadar.pdf Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201908). USENIX Association, 209\u2013224. http:\/\/www.usenix.org\/events\/osdi08\/tech\/full_papers\/cadar\/cadar.pdf"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9457-5"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863590"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034574.2034828"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408998"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993316.1993526"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596565"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3331545.3342589"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2016.22"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1449764.1449782"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03545-1_2"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_21"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360220"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434287"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480886"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45085-6_11"},{"key":"e_1_2_1_38_1","unstructured":"Ralf Hinze. 2000. Generic programs and proofs. Habilitation thesis. Universit\u00e4t Bonn. \t\t\t\t  Ralf Hinze. 2000. Generic programs and proofs. Habilitation thesis. Universit\u00e4t Bonn."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31113-0_16"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(86)90059-1"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796810000122"},{"key":"e_1_2_1_42_1","unstructured":"Sander Huyghebaert Dominique Devriese and Steven Keuchel. 2022. MinimalCaps Case Study. https:\/\/github.com\/katamaran-project\/katamaran\/tree\/v0.2\/case_study\/MinimalCaps \t\t\t\t  Sander Huyghebaert Dominique Devriese and Steven Keuchel. 2022. MinimalCaps Case Study. https:\/\/github.com\/katamaran-project\/katamaran\/tree\/v0.2\/case_study\/MinimalCaps"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44124-4_8"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17164-2_21"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-11(3:19)2015"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_1_47_1","unstructured":"Steven Keuchel Sander Huyghebaert Georgy Lukyanov and Dominique Devriese. 2022. Katamaran Development Repository. https:\/\/github.com\/katamaran-project\/katamaran\/ \t\t\t\t  Steven Keuchel Sander Huyghebaert Georgy Lukyanov and Dominique Devriese. 2022. Katamaran Development Repository. https:\/\/github.com\/katamaran-project\/katamaran\/"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.6865817"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-014-0326-7"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21437-0_14"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(96)00169-7"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236772"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2004.10.015"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03829-7_7"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199528"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341708"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006326"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/44501.44503"},{"key":"e_1_2_1_60_1","volume-title":"Programming from Specifications (2 ed.)","author":"Morgan Carroll","unstructured":"Carroll Morgan . 1994. Programming from Specifications (2 ed.) . Prentice Hall . isbn:978-0131232747 http:\/\/www.cs.ox.ac.uk\/publications\/books\/PfS\/ Carroll Morgan. 1994. Programming from Specifications (2 ed.). Prentice Hall. isbn:978-0131232747 http:\/\/www.cs.ox.ac.uk\/publications\/books\/PfS\/"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/69558.69559"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84628-692-6"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/1498926.1498929"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_33"},{"key":"e_1_2_1_66_1","volume-title":"Millennial Perspectives in Computer Science: Proceedings of the 1999 Oxford-Microsoft Symposium in honour of Sir Tony Hoare, J. Davies, B. Roscoe, and J. Woodcock (Eds.). Macmillan Education UK.","author":"Reynolds John C.","year":"2000","unstructured":"John C. Reynolds . 2000 . Intuitionistic reasoning about shared mutable data structure . In Millennial Perspectives in Computer Science: Proceedings of the 1999 Oxford-Microsoft Symposium in honour of Sir Tony Hoare, J. Davies, B. Roscoe, and J. Woodcock (Eds.). Macmillan Education UK. John C. Reynolds. 2000. Intuitionistic reasoning about shared mutable data structure. In Millennial Perspectives in Computer Science: Proceedings of the 1999 Oxford-Microsoft Symposium in honour of Sir Tony Hoare, J. Davies, B. Roscoe, and J. Woodcock (Eds.). Macmillan Education UK."},{"key":"e_1_2_1_67_1","volume-title":"The proof theory and semantics of intuitionistic modal logic. Ph. D. Dissertation","author":"Simpson Alex K","unstructured":"Alex K Simpson . 1994. The proof theory and semantics of intuitionistic modal logic. Ph. D. Dissertation . University of Edinburgh. Alex K Simpson. 1994. The proof theory and semantics of intuitionistic modal logic. Ph. D. Dissertation. University of Edinburgh."},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341690"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2491978"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133913"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.2307\/2271658"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_32"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341688"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/2393596.2393665"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-95891-8_51"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/1774088.1774610"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70594-9_20"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3547628","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3547628","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T18:43:29Z","timestamp":1750272209000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3547628"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,29]]},"references-count":78,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2022,8,29]]}},"alternative-id":["10.1145\/3547628"],"URL":"https:\/\/doi.org\/10.1145\/3547628","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,8,29]]},"assertion":[{"value":"2022-08-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}