{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T06:30:03Z","timestamp":1750746603304,"version":"3.41.0"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2023,8,30]],"date-time":"2023-08-30T00:00:00Z","timestamp":1693353600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100006195","name":"Ames Research Center","doi-asserted-by":"publisher","award":["80ARC020D0010"],"award-info":[{"award-number":["80ARC020D0010"]}],"id":[{"id":"10.13039\/100006195","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":[[2023,8,30]]},"abstract":"<jats:p>When runtime verification is used to monitor safety-critical systems, it is essential that monitoring code behaves correctly. The Copilot runtime verification framework pursues this goal by automatically generating C monitor programs from a high-level DSL embedded in Haskell. In safety-critical domains, every piece of deployed code must be accompanied by an assurance argument that is convincing to human auditors. However, it is difficult for auditors to determine with confidence that a compiled monitor cannot crash and implements the behavior required by the Copilot semantics.<\/jats:p>\n          <jats:p>In this paper we describe CopilotVerifier, which runs alongside the Copilot compiler, generating a proof of correctness for the compiled output. The proof establishes that a given Copilot monitor and its compiled form produce equivalent outputs on equivalent inputs, and that they either crash in identical circumstances or cannot crash. The proof takes the form of a bisimulation broken down into a set of verification conditions. We leverage two pieces of SMT-backed technology: the Crucible symbolic execution library for LLVM and the What4 solver interface library. Our results demonstrate that dramatically increased compiler assurance can be achieved at moderate cost by building on existing tools. This paves the way to our ultimate goal of generating formal assurance arguments that are convincing to human auditors.<\/jats:p>","DOI":"10.1145\/3607841","type":"journal-article","created":{"date-parts":[[2023,8,31]],"date-time":"2023-08-31T17:40:31Z","timestamp":1693503631000},"page":"305-321","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Trustworthy Runtime Verification via Bisimulation (Experience Report)"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-5642-5667","authenticated-orcid":false,"given":"Ryan G.","family":"Scott","sequence":"first","affiliation":[{"name":"Galois, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4439-0130","authenticated-orcid":false,"given":"Mike","family":"Dodds","sequence":"additional","affiliation":[{"name":"Galois, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9998-0269","authenticated-orcid":false,"given":"Ivan","family":"Perez","sequence":"additional","affiliation":[{"name":"KBR @ NASA Ames Research Center, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-8216-4996","authenticated-orcid":false,"given":"Alwyn E.","family":"Goodloe","sequence":"additional","affiliation":[{"name":"NASA Ames Research Center, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-8767-0639","authenticated-orcid":false,"given":"Robert","family":"Dockins","sequence":"additional","affiliation":[{"name":"Amazon, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,8,31]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_2_1_1_1","DOI":"10.1109\/ARITH.2011.40"},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_1","DOI":"10.1007\/978-3-030-81685-8_31"},{"doi-asserted-by":"publisher","key":"e_1_2_1_3_1","DOI":"10.1145\/3140587.3062358"},{"doi-asserted-by":"publisher","key":"e_1_2_1_4_1","DOI":"10.1145\/3371112"},{"doi-asserted-by":"publisher","key":"e_1_2_1_5_1","DOI":"10.1145\/3477041"},{"doi-asserted-by":"publisher","key":"e_1_2_1_6_1","DOI":"10.1145\/41625.41641"},{"doi-asserted-by":"publisher","key":"e_1_2_1_7_1","DOI":"10.1145\/3341704"},{"doi-asserted-by":"publisher","key":"e_1_2_1_8_1","DOI":"10.1007\/978-3-319-96142-2_26"},{"doi-asserted-by":"publisher","key":"e_1_2_1_9_1","DOI":"10.1145\/351240.351266"},{"doi-asserted-by":"publisher","key":"e_1_2_1_10_1","DOI":"10.1007\/978-3-540-24730-2_15"},{"doi-asserted-by":"publisher","key":"e_1_2_1_11_1","DOI":"10.1109\/DASC52595.2021.9594406"},{"doi-asserted-by":"publisher","key":"e_1_2_1_12_1","DOI":"10.1007\/978-3-030-55754-6_21"},{"doi-asserted-by":"publisher","key":"e_1_2_1_13_1","DOI":"10.1007\/978-3-319-06200-6_1"},{"volume-title":"Autonomy Research for Civil Aviation: Toward a New Era of Flight","author":"National Research Council. 2014.","unstructured":"National Research Council. 2014. Autonomy Research for Civil Aviation: Toward a New Era of Flight. The National Academies Press.","key":"e_1_2_1_14_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_15_1","DOI":"10.1007\/978-3-642-33826-7_16"},{"doi-asserted-by":"publisher","key":"e_1_2_1_16_1","DOI":"10.1109\/TIME.2005.26"},{"doi-asserted-by":"publisher","key":"e_1_2_1_17_1","DOI":"10.1007\/978-3-319-48869-1_5"},{"doi-asserted-by":"publisher","key":"e_1_2_1_18_1","DOI":"10.3233\/978-1-61499-207-3-141"},{"doi-asserted-by":"publisher","key":"e_1_2_1_19_1","DOI":"10.1145\/263244.263267"},{"unstructured":"Issue on Copilot GitHub. 2021. Basic example involving structs generates invalid C code. https:\/\/github.com\/Copilot-Language\/copilot\/issues\/275","key":"e_1_2_1_20_1"},{"unstructured":"Issue on Copilot GitHub. 2021. C translation doesn\u2019t correctly select operations based on types. https:\/\/github.com\/Copilot-Language\/copilot\/issues\/263","key":"e_1_2_1_21_1"},{"unstructured":"Issue on Copilot GitHub. 2021. copilot-c99: C99 and interpretation of signum behave inconsistently for 0 and NaN. https:\/\/github.com\/Copilot-Language\/copilot\/issues\/278","key":"e_1_2_1_22_1"},{"unstructured":"Issue on Copilot GitHub. 2021. Delaying streams of arrays or structs produces C code that fails to compile with Clang. https:\/\/github.com\/Copilot-Language\/copilot\/issues\/276","key":"e_1_2_1_23_1"},{"unstructured":"Issue on Copilot GitHub. 2021. Generated C code accesses stream buffer out of bounds. https:\/\/github.com\/Copilot-Language\/copilot\/issues\/238","key":"e_1_2_1_24_1"},{"unstructured":"Issue on Copilot GitHub. 2022. copilot-c99: appending values to a stream of arrays produces incorrect C99 code. https:\/\/github.com\/Copilot-Language\/copilot\/issues\/314","key":"e_1_2_1_25_1"},{"unstructured":"Issue on Copilot GitHub. 2022. copilot-c99: array has incomplete element type error when declaring stream with array of structs. https:\/\/github.com\/Copilot-Language\/copilot\/issues\/373","key":"e_1_2_1_26_1"},{"unstructured":"Issue on Copilot GitHub. 2022. copilot-c99: Streams of arrays result in C code with undefined behavior. https:\/\/github.com\/Copilot-Language\/copilot\/issues\/386","key":"e_1_2_1_27_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_28_1","DOI":"10.1007\/978-3-319-47166-2_31"},{"volume-title":"Monitoring Distributed Real-Time Systems: A Survey and Future Directions","author":"Goodloe Alwyn","unstructured":"Alwyn Goodloe and Lee Pike. 2010. Monitoring Distributed Real-Time Systems: A Survey and Future Directions. NASA Langley Research Center.","key":"e_1_2_1_29_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_30_1","DOI":"10.1007\/978-3-540-68524-1_3"},{"unstructured":"Joe Hendrix Ben Selfridge and Robert Dockins. 2020. What4: New Library to Help Developers Build Verification and Program Analysis Tools. https:\/\/galois.com\/blog\/2020\/07\/what4-new-library-to-help-devs-build-verification-program-tools\/","key":"e_1_2_1_31_1"},{"key":"e_1_2_1_32_1","volume-title":"Proceedings of the dependable systems and networks 2004 workshop on assurance cases. 6.","author":"Kelly Tim","year":"2004","unstructured":"Tim Kelly and Rob Weaver. 2004. The goal structuring notation\u2013a safety argument notation. In Proceedings of the dependable systems and networks 2004 workshop on assurance cases. 6."},{"doi-asserted-by":"publisher","key":"e_1_2_1_33_1","DOI":"10.1145\/2578855.2535841"},{"doi-asserted-by":"publisher","unstructured":"Jonathan Laurent Alwyn Goodloe and Lee Pike. 2015. Assuring the guardians. In Runtime Verification. 87\u2013101. https:\/\/doi.org\/10.1007\/978-3-319-23820-3_6 10.1007\/978-3-319-23820-3_6","key":"e_1_2_1_34_1","DOI":"10.1007\/978-3-319-23820-3_6"},{"doi-asserted-by":"publisher","key":"e_1_2_1_35_1","DOI":"10.1145\/1538788.1538814"},{"doi-asserted-by":"publisher","key":"e_1_2_1_36_1","DOI":"10.1145\/3453483.3454030"},{"volume-title":"Adding Runtime Verification to the Proteus Language. Ph. D. Dissertation","author":"McClelland Brian","unstructured":"Brian McClelland. 2021. Adding Runtime Verification to the Proteus Language. Ph. D. Dissertation. California State University, Northridge.","key":"e_1_2_1_37_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_38_1","DOI":"10.1109\/SMC-IT51442.2021.00010"},{"volume-title":"AFE 87 - Machine Learning","author":"Members Project","unstructured":"AFE87 Project Members. 2020. AFE 87 - Machine Learning. Aerospace Vehicle Systems Institute.","key":"e_1_2_1_39_1"},{"unstructured":"Ivan Perez Frank Dedden and Alwyn Goodloe. 2020. Copilot 3. NASA Langley Research Center.","key":"e_1_2_1_40_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_41_1","DOI":"10.1007\/978-3-030-99524-9_21"},{"doi-asserted-by":"publisher","key":"e_1_2_1_42_1","DOI":"10.1007\/978-3-642-16612-9_26"},{"doi-asserted-by":"publisher","key":"e_1_2_1_43_1","DOI":"10.1145\/2398856.2364553"},{"doi-asserted-by":"publisher","key":"e_1_2_1_44_1","DOI":"10.1007\/s11334-013-0223-x"},{"doi-asserted-by":"publisher","key":"e_1_2_1_45_1","DOI":"10.1007\/BFb0054170"},{"doi-asserted-by":"publisher","key":"e_1_2_1_46_1","DOI":"10.1145\/2854065.2854066"},{"volume-title":"Formal Methods Supplement to DO-178C and DO-278A. RTCA","unstructured":"2011. Formal Methods Supplement to DO-178C and DO-278A. RTCA, Inc.. RCTA\/DO333","key":"e_1_2_1_47_1"},{"volume-title":"Software Considerations in Airborne Systems and Equipment Certification. RTCA","author":"RTCA.","unstructured":"RTCA. 2011. Software Considerations in Airborne Systems and Equipment Certification. RTCA, Inc.. RCTA\/DO-178C","key":"e_1_2_1_48_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_49_1","DOI":"10.1007\/978-3-642-02658-4_57"},{"unstructured":"SAE International. 2010. Guidelines For Development Of Civil Aircraft and Systems. SAE International. ARP4754A","key":"e_1_2_1_50_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_51_1","DOI":"10.5281\/zenodo.6147218"},{"doi-asserted-by":"publisher","unstructured":"Ryan G. Scott Mike Dodds Ivan Perez Alwyn E. Goodloe and Robert Dockins. 2023. Artifact for \"Trustworthy Runtime Verification via Bisimulation (Experience Report)\". https:\/\/doi.org\/10.5281\/zenodo.7978326 10.5281\/zenodo.7978326","key":"e_1_2_1_52_1","DOI":"10.5281\/zenodo.7978326"},{"key":"e_1_2_1_53_1","volume-title":"Crux: Introducing Our New Open-Source Tool for Software Verification. https:\/\/galois.com\/blog\/2020\/10\/crux-introducing-our-new-open-source-tool-for-software-verification\/","author":"Tomb Aaron","year":"2020","unstructured":"Aaron Tomb. 2020. Crux: Introducing Our New Open-Source Tool for Software Verification. https:\/\/galois.com\/blog\/2020\/10\/crux-introducing-our-new-open-source-tool-for-software-verification\/"},{"volume-title":"Analysis of Well-Clear Boundary Models for the Integration of UAS in the NAS","author":"Upchurch Jason M","unstructured":"Jason M Upchurch, Cesar A Munoz, Anthony J Narkawicz, James P Chamberlain, and Maria C Consiglio. 2014. Analysis of Well-Clear Boundary Models for the Integration of UAS in the NAS. NASA Langley Research Center.","key":"e_1_2_1_54_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_55_1","DOI":"10.1007\/978-3-319-57288-8_29"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3607841","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3607841","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3607841","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:37:06Z","timestamp":1750178226000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3607841"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,8,30]]},"references-count":55,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2023,8,30]]}},"alternative-id":["10.1145\/3607841"],"URL":"https:\/\/doi.org\/10.1145\/3607841","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2023,8,30]]},"assertion":[{"value":"2023-08-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}