{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T04:55:34Z","timestamp":1777524934598,"version":"3.51.4"},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T00:00:00Z","timestamp":1648598400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T00:00:00Z","timestamp":1648598400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100002790","name":"Canadian Network for Research and Innovation in Machining Technology, Natural Sciences and Engineering Research Council of Canada","doi-asserted-by":"publisher","award":["543583-19"],"award-info":[{"award-number":["543583-19"]}],"id":[{"id":"10.13039\/501100002790","id-type":"DOI","asserted-by":"publisher"}]},{"name":"WATERLOO-HUAWEI JOINT INNOVATION LAB"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2022,9]]},"DOI":"10.1007\/s11334-022-00443-9","type":"journal-article","created":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T09:04:46Z","timestamp":1648631086000},"page":"335-346","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Verifying verified code"],"prefix":"10.1007","volume":"18","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2172-9525","authenticated-orcid":false,"given":"Siddharth","family":"Priya","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiang","family":"Zhou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yusen","family":"Su","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yakir","family":"Vizel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuyan","family":"Bao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arie","family":"Gurfinkel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,3,30]]},"reference":[{"key":"443_CR1","doi-asserted-by":"crossref","unstructured":"Rakamaric Z, Emmi M (2014) SMACK: decoupling source language details from verifier implementations. In: Computer aided verification\u201426th international conference, CAV 2014, held as part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings. Lecture notes in computer science, vol 8559, pp 106\u2013113","DOI":"10.1007\/978-3-319-08867-9_7"},{"key":"443_CR2","doi-asserted-by":"crossref","unstructured":"Beyer D, Keremoglu ME (2011) CPAchecker: a tool for configurable software verification. In: Computer aided verification\u201423rd international conference, CAV 2011, Snowbird, UT, USA, July 14\u201320, 2011. Proceedings. Lecture notes in computer science, vol 6806, pp 184\u2013190","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"443_CR3","doi-asserted-by":"crossref","unstructured":"Gadelha MYR, Monteiro FR, Morse J, Cordeiro LC, Fischer B, Nicole DA (2018) ESBMC 5.0: an industrial-strength C model checker. In: Proceedings of the 33rd ACM\/IEEE international conference on automated software engineering, ASE 2018, Montpellier, France, September 3\u20137, 2018, pp 888\u2013891","DOI":"10.1145\/3238147.3240481"},{"key":"443_CR4","doi-asserted-by":"crossref","unstructured":"Lal A, Qadeer S (2014) Powering the static driver verifier using Corral. In: Proceedings of the 22nd ACM SIGSOFT international symposium on Foundations of Software Engineering, (FSE-22), Hong Kong, China, November 16\u201322, 2014, pp 202\u2013212","DOI":"10.1145\/2635868.2635894"},{"key":"443_CR5","doi-asserted-by":"crossref","unstructured":"Ivancic F, Yang Z, Ganai MK, Gupta A, Shlyakhter I, Ashar P (2005) F-Soft: software verification platform. In: Computer aided verification, 17th international conference, CAV 2005, Edinburgh, Scotland, UK, July 6\u201310, 2005, Proceedings. Lecture notes in computer science, vol 3576, pp 301\u2013306","DOI":"10.1007\/11513988_31"},{"key":"443_CR6","doi-asserted-by":"crossref","unstructured":"Clarke EM, Kroening D, Lerda F (2004) A tool for checking ANSI-C programs. In: 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. Lecture notes in computer science, vol 2988, pp 168\u2013176","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"443_CR7","unstructured":"Galois: Crux: a tool for improving the assurance of software using symbolic testing. https:\/\/crux.galois.com\/"},{"key":"443_CR8","doi-asserted-by":"crossref","unstructured":"B\u00fcning MK, Sinz C, Farag\u00f3 D (2020) QPR verify: a static analysis tool for embedded software based on bounded model checking. In: Software verification\u201412th international conference, VSTTE 2020, and 13th international workshop, NSV 2020, Los Angeles, CA, USA, July 20\u201321, 2020, revised selected papers. Lecture notes in computer science, vol 12549, pp 21\u201332","DOI":"10.1007\/978-3-030-63618-0_2"},{"key":"443_CR9","doi-asserted-by":"crossref","unstructured":"Beyer D (2020) Advances in automatic software verification: SV-COMP 2020. In: Tools and algorithms for the construction and analysis of systems\u201426th international conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25\u201330, 2020, Proceedings, Part II. Lecture notes in computer science, vol 12079, pp 347\u2013367","DOI":"10.1007\/978-3-030-45237-7_21"},{"key":"443_CR10","unstructured":"Serebryany K.: libFuzzer: a library for coverage-guided fuzz testing. https:\/\/llvm.org\/docs\/LibFuzzer.html"},{"issue":"2","key":"443_CR11","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/1646353.1646374","volume":"53","author":"A Bessey","year":"2010","unstructured":"Bessey A, Block K, Chelf B, Chou A, Fulton B, Hallem S, Gros C, Kamsky A, McPeak S, Engler DR (2010) A few billion lines of code later: using static analysis to find bugs in the real world. Commun ACM 53(2):66\u201375","journal-title":"Commun ACM"},{"key":"443_CR12","doi-asserted-by":"crossref","unstructured":"Chong N, Cook B, Kallas K, Khazem K, Monteiro FR, Schwartz-Narbonne D, Tasiran S, Tautschnig M, Tuttle MR (2020) Code-level model checking in the software development workflow. In: ICSE-SEIP 2020: 42nd international conference on software engineering, software engineering in practice, Seoul, South Korea, 27 June\u201319 July, 2020, pp 11\u201320","DOI":"10.1145\/3377813.3381347"},{"key":"443_CR13","doi-asserted-by":"crossref","unstructured":"Gurfinkel A, Kahsai T, Komuravelli A, Navas JA (2015) The SeaHorn verification framework. In: Computer aided verification\u201427th international conference, CAV 2015, San Francisco, CA, USA, July 18\u201324, 2015, Proceedings, Part I. Lecture notes in computer science, vol 9206, pp 343\u2013361","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"443_CR14","unstructured":"Cadar C, Dunbar D, Engler DR (2008) KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: 8th USENIX symposium on operating systems design and implementation, OSDI 2008, December 8\u201310, 2008, San Diego, California, USA, Proceedings, pp 209\u2013224"},{"key":"443_CR15","unstructured":"Osherove R (2009) The art of unit testing: with examples in .Net"},{"key":"443_CR16","doi-asserted-by":"crossref","unstructured":"Lattner C, Adve VS (2004) LLVM: a compilation framework for lifelong program analysis & transformation. In: 2nd IEEE\/ACM international symposium on code generation and optimization (CGO 2004), 20\u201324 March 2004, San Jose, CA, USA, pp 75\u201388","DOI":"10.1109\/CGO.2004.1281665"},{"key":"443_CR17","unstructured":"uClibc is a small C standard library. https:\/\/www.uclibc.org\/"},{"key":"443_CR18","doi-asserted-by":"crossref","unstructured":"Memarian K, Matthiesen J, Lingard J, Nienhuis K, Chisnall D, Watson RNM, Sewell P (2016) Into the depths of C: elaborating the de facto standards. In: Proceedings of the 37th ACM SIGPLAN conference on programming language design and implementation, PLDI 2016, Santa Barbara, CA, USA, June 13\u201317, 2016, pp 1\u201315","DOI":"10.1145\/2908080.2908081"},{"key":"443_CR19","doi-asserted-by":"crossref","unstructured":"Kocher P, Genkin D, Gruss D, Haas W, Hamburg M, Lipp M, Mangard S, Prescher T, Schwarz M, Yarom Y (2018) Spectre attacks: exploiting speculative execution. meltdownattack.com","DOI":"10.1109\/SP.2019.00002"},{"key":"443_CR20","unstructured":"Moy Y, Wallenburg A (2010) Tokeneer: beyond formal program verification. In: Embedded real time software and systems, vol 24"},{"key":"443_CR21","doi-asserted-by":"crossref","unstructured":"Kupferman O (2006) Sanity checks in formal verification. In: CONCUR 2006\u2014concurrency theory, 17th international conference, CONCUR 2006, Bonn, Germany, August 27\u201330, 2006, Proceedings. Lecture notes in computer science, vol 4137, pp 37\u201351","DOI":"10.1007\/11817949_3"},{"key":"443_CR22","unstructured":"Serebryany K, Bruening D, Potapenko A, Vyukov D (2012) Addresssanitizer: a fast address sanity checker. In: Heiser G, Hsieh WC (eds) 2012 USENIX annual technical conference, Boston, MA, USA, June 13\u201315, 2012, pp 309\u2013318. https:\/\/www.usenix.org\/conference\/atc12\/technical-sessions\/presentation\/serebryany"},{"key":"443_CR23","doi-asserted-by":"crossref","unstructured":"Kim Y, Kim M (2014) SAT-based bounded software model checking for embedded software: a case study. In: 21st Asia-Pacific Software Engineering Conference, APSEC 2014, Jeju, South Korea, December 1\u20134, 2014. Volume 1: research papers, pp 55\u201362","DOI":"10.1109\/APSEC.2014.17"},{"key":"443_CR24","doi-asserted-by":"crossref","unstructured":"Cook B, Khazem K, Kroening D, Tasiran S, Tautschnig M, Tuttle MR (2018) Model checking boot code from AWS data centers. In: Computer aided verification\u201430th international conference, CAV 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 14\u201317, 2018, Proceedings, Part II. Lecture notes in computer science, vol 10982, pp 467\u2013486. https:\/\/OPTdoi.org\/10.1007\/978-3-319-96142-2_28","DOI":"10.1007\/978-3-319-96142-2_28"},{"key":"443_CR25","doi-asserted-by":"crossref","unstructured":"Chudnov A, Collins N, Cook B, Dodds J, Huffman B, MacC\u00e1rthaigh C, Magill S, Mertens E, Mullen E, Tasiran S, Tomb A, Westbrook E (2018) Continuous formal verification of Amazon s2n. In: Computer aided verification\u201430th international conference, CAV 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 14\u201317, 2018, Proceedings, Part II. Lecture notes in computer science, vol 10982, pp 430\u2013446","DOI":"10.1007\/978-3-319-96142-2_26"},{"key":"443_CR26","unstructured":"Cook B, D\u00f6bel B, Kroening D, Manthey N, Pohlack M, Polgreen E, Tautschnig M, Wieczorkiewicz P (2020) Using model checking tools to triage the severity of security bugs in the Xen hypervisor. In: 2020 formal methods in computer aided design, FMCAD 2020, Haifa, Israel, September 21\u201324, 2020, pp 185\u2013193. https:\/\/OPTdoi.org\/10.34727\/2020\/isbn.978-3-85448-042-6_26"},{"key":"443_CR27","doi-asserted-by":"publisher","unstructured":"F\u00e4hndrich M, Barnett M, Logozzo F.: Embedded contract languages. In: Shin SY, Ossowski S, Schumacher M, Palakal MJ, Hung C (eds) Proceedings of the 2010 ACM Symposium on Applied Computing (SAC), Sierre, Switzerland, March 22\u201326, 2010, pp 2103\u20132110. https:\/\/doi.org\/10.1145\/1774088.1774531","DOI":"10.1145\/1774088.1774531"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-022-00443-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11334-022-00443-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-022-00443-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,12]],"date-time":"2022-09-12T06:44:55Z","timestamp":1662965095000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11334-022-00443-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,3,30]]},"references-count":27,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2022,9]]}},"alternative-id":["443"],"URL":"https:\/\/doi.org\/10.1007\/s11334-022-00443-9","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,3,30]]},"assertion":[{"value":"22 October 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 February 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 March 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}