{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,21]],"date-time":"2026-03-21T03:17:21Z","timestamp":1774063041218,"version":"3.50.1"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030888848","type":"print"},{"value":"9783030888855","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-88885-5_13","type":"book-chapter","created":{"date-parts":[[2021,10,13]],"date-time":"2021-10-13T17:25:06Z","timestamp":1634145906000},"page":"187-202","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Verifying Verified Code"],"prefix":"10.1007","author":[{"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":[[2021,10,12]]},"reference":[{"issue":"6","key":"13_CR1","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1145\/1953122.1953145","volume":"54","author":"M Barnett","year":"2011","unstructured":"Barnett, M., F\u00e4hndrich, M., Leino, K.R.M., M\u00fcller, P., Schulte, W., Venter, H.: Specification and verification: the Spec# experience. Commun. ACM 54(6), 81\u201391 (2011)","journal-title":"Commun. ACM"},{"key":"13_CR2","doi-asserted-by":"publisher","unstructured":"Bessey, A., et al.: A few billion lines of code later: using static analysis to find bugs in the real world. Commun. ACM 53(2), 66\u201375 (2010). https:\/\/doi.org\/10.1145\/1646353.1646374","DOI":"10.1145\/1646353.1646374"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/978-3-030-45237-7_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Beyer","year":"2020","unstructured":"Beyer, D.: Advances in automatic software verification: SV-COMP 2020. In: TACAS 2020. LNCS, vol. 12079, pp. 347\u2013367. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45237-7_21"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Computer Aided Verification","author":"D Beyer","year":"2011","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184\u2013190. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-030-63618-0_2","volume-title":"Software Verification","author":"M Kleine B\u00fcning","year":"2020","unstructured":"Kleine B\u00fcning, M., Sinz, C., Farag\u00f3, D.: QPR verify: a static analysis tool for\u00a0embedded software based on bounded model checking. In: Christakis, M., Polikarpova, N., Duggirala, P.S., Schrammel, P. (eds.) NSV\/VSTTE -2020. LNCS, vol. 12549, pp. 21\u201332. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-63618-0_2"},{"key":"13_CR6","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: 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, 8\u201310 December 2008, San Diego, California, USA, Proceedings, pp. 209\u2013224. USENIX Association (2008)"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Chong, N., et al.: 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. ACM (2020)","DOI":"10.1145\/3377813.3381347"},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/978-3-319-96142-2_26","volume-title":"Computer Aided Verification","author":"A Chudnov","year":"2018","unstructured":"Chudnov, A., et al.: Continuous formal verification of Amazon s2n. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 430\u2013446. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_26"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168\u2013176. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_15"},{"key":"13_CR10","doi-asserted-by":"publisher","unstructured":"Cook, B., et al.: 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, 21\u201324 September 2020, pp. 185\u2013193. IEEE (2020). https:\/\/doi.org\/10.34727\/2020\/isbn.978-3-85448-042-6_26","DOI":"10.34727\/2020\/isbn.978-3-85448-042-6_26"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1007\/978-3-319-96142-2_28","volume-title":"Computer Aided Verification","author":"B Cook","year":"2018","unstructured":"Cook, B., Khazem, K., Kroening, D., Tasiran, S., Tautschnig, M., Tuttle, M.R.: Model checking boot code from AWS data centers. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 467\u2013486. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_28"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"Gadelha, M.Y.R., Monteiro, F.R., Morse, J., Cordeiro, L.C., Fischer, B., Nicole, D.A.: 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, 3\u20137 September 2018, pp. 888\u2013891. ACM (2018)","DOI":"10.1145\/3238147.3240481"},{"key":"13_CR13","unstructured":"Galois: Crux: A Tool for Improving the Assurance of Software Using Symbolic Testing. https:\/\/crux.galois.com\/"},{"key":"13_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-319-21690-4_20","volume-title":"Computer Aided Verification","author":"A Gurfinkel","year":"2015","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The seahorn verification framework. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343\u2013361. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_20"},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/11513988_31","volume-title":"Computer Aided Verification","author":"F Ivan\u010di\u0107","year":"2005","unstructured":"Ivan\u010di\u0107, F., Yang, Z., Ganai, M.K., Gupta, A., Shlyakhter, I., Ashar, P.: F-Soft: software verification platform. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 301\u2013306. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11513988_31"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"Kim, Y., Kim, M.: SAT-based bounded software model checking for embedded software: a case study. In: 21st Asia-Pacific Software Engineering Conference, APSEC 2014, Jeju, South Korea, 1\u20134 December 2014. Volume 1: Research Papers, pp. 55\u201362. IEEE Computer Society (2014)","DOI":"10.1109\/APSEC.2014.17"},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"Kocher, P., et al.: Spectre attacks: exploiting speculative execution (2018). http:\/\/meltdownattack.com\/","DOI":"10.1109\/SP.2019.00002"},{"key":"13_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/11817949_3","volume-title":"CONCUR 2006 \u2013 Concurrency Theory","author":"O Kupferman","year":"2006","unstructured":"Kupferman, O.: Sanity checks in formal verification. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 37\u201351. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817949_3"},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"Lal, A., Qadeer, S.: 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, 16\u201322 November 2014, pp. 202\u2013212. ACM (2014)","DOI":"10.1145\/2635868.2635894"},{"key":"13_CR20","unstructured":"Lattner, C., Adve, V.S.: 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. IEEE Computer Society (2004)"},{"key":"13_CR21","doi-asserted-by":"crossref","unstructured":"Memarian, K., et al.: 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, 13\u201317 June 2016, pp. 1\u201315. ACM (2016)","DOI":"10.1145\/2908080.2908081"},{"key":"13_CR22","unstructured":"Moy, Y., Wallenburg, A.: Tokeneer: beyond formal program verification. Embed. Real Time Softw. Syst. 24 (2010)"},{"key":"13_CR23","unstructured":"Osherove, R.: The Art of Unit Testing: With Examples in .Net. Manning PublicationsCo., Shelter Island (2009)"},{"key":"13_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/978-3-319-08867-9_7","volume-title":"Computer Aided Verification","author":"Z Rakamari\u0107","year":"2014","unstructured":"Rakamari\u0107, Z., Emmi, M.: SMACK: decoupling source language details from verifier implementations. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 106\u2013113. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_7"},{"key":"13_CR25","unstructured":"Serebryany, K.: libFuzzer: a library for coverage-guided fuzz testing. https:\/\/llvm.org\/docs\/LibFuzzer.html"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-88885-5_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,13]],"date-time":"2021-10-13T18:00:26Z","timestamp":1634148026000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-88885-5_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030888848","9783030888855"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-88885-5_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"12 October 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ATVA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Automated Technology for Verification and Analysis","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Gold Coast, QLD","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Australia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 October 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 October 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"atva2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/formal-analysis.com\/atva\/2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"75","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"19","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"25% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"In addition there are 4 tool papers. The conference was held online because of the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}