{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,20]],"date-time":"2026-03-20T16:57:03Z","timestamp":1774025823351,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":42,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,6,18]],"date-time":"2021-06-18T00:00:00Z","timestamp":1623974400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,6,19]]},"DOI":"10.1145\/3453483.3454065","type":"proceedings-article","created":{"date-parts":[[2021,6,18]],"date-time":"2021-06-18T13:51:32Z","timestamp":1624024292000},"page":"604-619","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":23,"title":["Integration verification across software and hardware for a simple embedded system"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9854-7500","authenticated-orcid":false,"given":"Andres","family":"Erbsen","sequence":"first","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8369-9117","authenticated-orcid":false,"given":"Samuel","family":"Gruetter","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1084-881X","authenticated-orcid":false,"given":"Joonwon","family":"Choi","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]},{"given":"Clark","family":"Wood","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]},{"given":"Adam","family":"Chlipala","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]}],"member":"320","published-online":{"date-parts":[[2021,6,18]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Proceedings of 4th International Verification Workshop in Connection with CADE-21","volume":"04","author":"Alkassar Eyad","year":"2007","unstructured":"Eyad Alkassar , Mark A. Hillebrand , Steffen Knapp , Rostislav Rusev , and Sergey Tverdyshev . 2007 . Formal Device and Programming Model for a Serial Interface . In Proceedings of 4th International Verification Workshop in Connection with CADE-21 , Bremen, Germany , July 15-16, 2007, Bernhard Beckert (Ed.) (CEUR Workshop Proceedings, Vol. 259). CEUR-WS.org. http:\/\/ceur-ws.org\/Vol-259\/paper 04 .pdf Eyad Alkassar, Mark A. Hillebrand, Steffen Knapp, Rostislav Rusev, and Sergey Tverdyshev. 2007. Formal Device and Programming Model for a Serial Interface. In Proceedings of 4th International Verification Workshop in Connection with CADE-21, Bremen, Germany, July 15-16, 2007, Bernhard Beckert (Ed.) (CEUR Workshop Proceedings, Vol. 259). CEUR-WS.org. http:\/\/ceur-ws.org\/Vol-259\/paper04.pdf"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87873-5_18"},{"key":"e_1_3_2_1_3_1","volume-title":"Program Logics - for Certified Compilers","author":"Appel Andrew W.","unstructured":"Andrew W. Appel . 2014. Program Logics - for Certified Compilers . Cambridge University Press . isbn:978-1-10-704801-0 https:\/\/www.cs.princeton.edu\/~appel\/papers\/plcc.pdf Andrew W. Appel. 2014. Program Logics - for Certified Compilers. Cambridge University Press. isbn:978-1-10-704801-0 https:\/\/www.cs.princeton.edu\/~appel\/papers\/plcc.pdf"},{"key":"e_1_3_2_1_4_1","volume-title":"The Rocket Chip Generator. EECS Department","author":"Asanovi\u0107 Krste","year":"2016","unstructured":"Krste Asanovi\u0107 , Rimas Avizienis , Jonathan Bachrach , Scott Beamer , David Biancolin , Christopher Celio , Henry Cook , Daniel Dabbelt , John Hauser , Adam Izraelevitz , Sagar Karandikar , Ben Keller , Donggyu Kim , John Koenig , Yunsup Lee , Eric Love , Martin Maas , Albert Magyar , Howard Mao , Miquel Moreto , Albert Ou , David A. Patterson , Brian Richards , Colin Schmidt , Stephen Twigg , Huy Vo , and Andrew Waterman . 2016. The Rocket Chip Generator. EECS Department , University of California , Berkeley. http:\/\/www2.eecs.berkeley.edu\/Pubs\/TechRpts\/ 2016 \/EECS-2016-17.html Krste Asanovi\u0107, Rimas Avizienis, Jonathan Bachrach, Scott Beamer, David Biancolin, Christopher Celio, Henry Cook, Daniel Dabbelt, John Hauser, Adam Izraelevitz, Sagar Karandikar, Ben Keller, Donggyu Kim, John Koenig, Yunsup Lee, Eric Love, Martin Maas, Albert Magyar, Howard Mao, Miquel Moreto, Albert Ou, David A. Patterson, Brian Richards, Colin Schmidt, Stephen Twigg, Huy Vo, and Andrew Waterman. 2016. The Rocket Chip Generator. EECS Department, University of California, Berkeley. http:\/\/www2.eecs.berkeley.edu\/Pubs\/TechRpts\/2016\/EECS-2016-17.html"},{"key":"e_1_3_2_1_5_1","volume-title":"Young","author":"Bevier William R.","year":"1989","unstructured":"William R. Bevier , Warren A. Hunt , Jr., J. Strother Moore , and William D . Young . 1989 . An approach to systems verification. J. Autom. Reasoning , 411\u2013428. https:\/\/citeseerx.ist.psu.edu\/viewdoc\/download?doi=10.1.1.68.6467&rep=rep1&type=pdf William R. Bevier, Warren A. Hunt, Jr., J. Strother Moore, and William D. Young. 1989. An approach to systems verification. J. Autom. Reasoning, 411\u2013428. https:\/\/citeseerx.ist.psu.edu\/viewdoc\/download?doi=10.1.1.68.6467&rep=rep1&type=pdf"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL.2017.1"},{"key":"e_1_3_2_1_7_1","unstructured":"Thomas Bourgeat Ian Clester Andres Erbsen Samuel Gruetter Andrew Wright and Adam Chlipala. 2021. A Multipurpose Formal RISC-V Specification. arxiv:2104.00762.  Thomas Bourgeat Ian Clester Andres Erbsen Samuel Gruetter Andrew Wright and Adam Chlipala. 2021. A Multipurpose Formal RISC-V Specification. arxiv:2104.00762."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236784"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250743"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110268"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9458-4"},{"key":"e_1_3_2_1_12_1","volume-title":"Proc","author":"Daum Matthias","unstructured":"Matthias Daum , Norbert W. Schirmer , and Mareike Schmidt . 2010. From operating-system correctness to pervasively verified applications . In Proc . IFM. Springer-Verlag , 105\u2013120. https:\/\/hal.inria.fr\/inria-00524575\/document Matthias Daum, Norbert W. Schirmer, and Mareike Schmidt. 2010. From operating-system correctness to pervasively verified applications. In Proc. IFM. Springer-Verlag, 105\u2013120. https:\/\/hal.inria.fr\/inria-00524575\/document"},{"key":"e_1_3_2_1_13_1","unstructured":"George Dunlap. 2012. The Intel SYSRET privilege escalation. https:\/\/xenproject.org\/2012\/06\/13\/the-intel-sysret-privilege-escalation\/  George Dunlap. 2012. The Intel SYSRET privilege escalation. https:\/\/xenproject.org\/2012\/06\/13\/the-intel-sysret-privilege-escalation\/"},{"key":"e_1_3_2_1_14_1","unstructured":"Alex Dzyoba. 2014. A tale about data corruption stack and red zone. https:\/\/alex.dzyoba.com\/blog\/redzone\/  Alex Dzyoba. 2014. A tale about data corruption stack and red zone. https:\/\/alex.dzyoba.com\/blog\/redzone\/"},{"key":"e_1_3_2_1_15_1","volume-title":"SMTCoq: A Plug-In for Integrating SMT Solvers into Coq","author":"Ekici Burak","unstructured":"Burak Ekici , Alain Mebsout , Cesare Tinelli , Chantal Keller , Guy Katz , Andrew Reynolds , and Clark Barrett . 2017. SMTCoq: A Plug-In for Integrating SMT Solvers into Coq . In Computer Aided Verification, Rupak Majumdar and Viktor Kun\u010dak (Eds.). 10427, Springer International Publishing , 126\u2013133. isbn:978-3-319-63389-3 978-3-319-63390-9 https:\/\/homepage.divms.uiowa.edu\/~tinelli\/papers\/EkiEtAl-CAV-17.pdf Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, and Clark Barrett. 2017. SMTCoq: A Plug-In for Integrating SMT Solvers into Coq. In Computer Aided Verification, Rupak Majumdar and Viktor Kun\u010dak (Eds.). 10427, Springer International Publishing, 126\u2013133. isbn:978-3-319-63389-3 978-3-319-63390-9 https:\/\/homepage.divms.uiowa.edu\/~tinelli\/papers\/EkiEtAl-CAV-17.pdf"},{"key":"e_1_3_2_1_16_1","volume-title":"\u201cOptimization","author":"Ertl M. Anton","year":"2015","unstructured":"M. Anton Ertl . 2015. What every compiler writer should know about programmers or \u201cOptimization \u201d based on undefined behaviour hurts performance. http:\/\/www.complang.tuwien.ac.at\/kps 2015 \/proceedings\/KPS_2015_submission_29.pdf M. Anton Ertl. 2015. What every compiler writer should know about programmers or \u201cOptimization\u201d based on undefined behaviour hurts performance. http:\/\/www.complang.tuwien.ac.at\/kps2015\/proceedings\/KPS_2015_submission_29.pdf"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132782"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676975"},{"key":"e_1_3_2_1_19_1","volume-title":"Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201916)","author":"Gu Ronghui","year":"2016","unstructured":"Ronghui Gu , Zhong Shao , Hao Chen , Xiongnan Wu , Jieung Kim , Vilhelm Sj\u00f6berg , and David Costanzo . 2016 . CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels . In Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201916) . USENIX Association, USA. 653\u2013669. isbn:978 1931971331 https:\/\/www.usenix.org\/conference\/osdi16\/technical-sessions\/presentation\/gu Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Wu, Jieung Kim, Vilhelm Sj\u00f6berg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201916). USENIX Association, USA. 653\u2013669. isbn:9781931971331 https:\/\/www.usenix.org\/conference\/osdi16\/technical-sessions\/presentation\/gu"},{"key":"e_1_3_2_1_20_1","volume-title":"11th USENIX Symposium on Operating Systems Design and Implementation (OSDI 14)","author":"Hawblitzel Chris","year":"2014","unstructured":"Chris Hawblitzel , Jon Howell , Jacob R. Lorch , Arjun Narayan , Bryan Parno , Danfeng Zhang , and Brian Zill . 2014 . Ironclad Apps: End-to-End Security via Automated Full-System Verification . In 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI 14) . USENIX Association, Broomfield, CO. 165\u2013181. isbn:978-1-93 1971-16-4 https:\/\/www.usenix.org\/conference\/osdi14\/technical-sessions\/presentation\/hawblitzel Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang, and Brian Zill. 2014. Ironclad Apps: End-to-End Security via Automated Full-System Verification. In 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI 14). USENIX Association, Broomfield, CO. 165\u2013181. isbn:978-1-931971-16-4 https:\/\/www.usenix.org\/conference\/osdi14\/technical-sessions\/presentation\/hawblitzel"},{"key":"e_1_3_2_1_21_1","unstructured":"Warren A. Hunt. 1989. Microprocessor Design Verification. http:\/\/www.cs.utexas.edu\/users\/boyer\/ftp\/cli-reports\/048.pdf  Warren A. Hunt. 1989. Microprocessor Design Verification. http:\/\/www.cs.utexas.edu\/users\/boyer\/ftp\/cli-reports\/048.pdf"},{"key":"e_1_3_2_1_22_1","unstructured":"SiFive Inc.. 2019. SiFive FE310-G000 Manual (v3p1). Available under \u201cFreedom E310-G000\u201d at https:\/\/www.sifive.com\/documentation  SiFive Inc.. 2019. SiFive FE310-G000 Manual (v3p1). Available under \u201cFreedom E310-G000\u201d at https:\/\/www.sifive.com\/documentation"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294106"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_3_2_1_26_1","unstructured":"Adam Langley. 2016. memcpy (and friends) with NULL pointers. https:\/\/www.imperialviolet.org\/2016\/06\/26\/nonnull.html  Adam Langley. 2016. memcpy (and friends) with NULL pointers. https:\/\/www.imperialviolet.org\/2016\/06\/26\/nonnull.html"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314622"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_16"},{"key":"e_1_3_2_1_31_1","volume-title":"ISO SC22 WG14 N2015","author":"Memarian Kayvan","year":"2016","unstructured":"Kayvan Memarian and Peter Sewell . 2016 . What is C in practice? (Cerberus survey v2): Analysis of Responses \u2013 with Comments . ISO SC22 WG14 N2015 . http:\/\/www.cl.cam.ac.uk\/~pes20\/cerberus\/analysis-2016-02-05-anon.txt Kayvan Memarian and Peter Sewell. 2016. What is C in practice? (Cerberus survey v2): Analysis of Responses \u2013 with Comments. ISO SC22 WG14 N2015. http:\/\/www.cl.cam.ac.uk\/~pes20\/cerberus\/analysis-2016-02-05-anon.txt"},{"key":"e_1_3_2_1_32_1","volume-title":"Gordon","author":"Myreen Magnus O.","year":"2007","unstructured":"Magnus O. Myreen and Michael J. C . Gordon . 2007 . Hoare logic for realistically modelled machine code. In In Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2007), LNCS. Springer-Verlag , 568\u2013582. http:\/\/citeseerx.ist.psu.edu\/viewdoc\/summary?doi=10.1.1.96.2793 Magnus O. Myreen and Michael J. C. Gordon. 2007. Hoare logic for realistically modelled machine code. In In Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2007), LNCS. Springer-Verlag, 568\u2013582. http:\/\/citeseerx.ist.psu.edu\/viewdoc\/summary?doi=10.1.1.96.2793"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359641"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132748"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.214687"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2487241.2487248"},{"key":"e_1_3_2_1_37_1","volume-title":"an Open Source Framework from Verilog to Bitstream for Commercial FPGAs. arxiv:1903.10407. 4 page short paper at IEEE FCCM","author":"Shah David","year":"2019","unstructured":"David Shah , Eddie Hung , Clifford Wolf , Serge Bazanski , Dan Gisselquist , and Miodrag Milanovi\u0107 . 2019. Yosys+nextpnr : an Open Source Framework from Verilog to Bitstream for Commercial FPGAs. arxiv:1903.10407. 4 page short paper at IEEE FCCM 2019 . David Shah, Eddie Hung, Clifford Wolf, Serge Bazanski, Dan Gisselquist, and Miodrag Milanovi\u0107. 2019. Yosys+nextpnr: an Open Source Framework from Verilog to Bitstream for Commercial FPGAs. arxiv:1903.10407. 4 page short paper at IEEE FCCM 2019."},{"key":"e_1_3_2_1_38_1","volume-title":"Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201918)","author":"Sigurbjarnarson Helgi","year":"2018","unstructured":"Helgi Sigurbjarnarson , Luke Nelson , Bruno Castro-Karney , James Bornholt , Emina Torlak , and Xi Wang . 2018 . Nickel: A Framework for Design and Verification of Information Flow Control Systems . In Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201918) . USENIX Association, USA. 287\u2013305. isbn:978 1931971478 https:\/\/unsat.cs.washington.edu\/papers\/sigurbjarnarson-nickel.pdf Helgi Sigurbjarnarson, Luke Nelson, Bruno Castro-Karney, James Bornholt, Emina Torlak, and Xi Wang. 2018. Nickel: A Framework for Design and Verification of Information Flow Control Systems. In Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201918). USENIX Association, USA. 287\u2013305. isbn:9781931971478 https:\/\/unsat.cs.washington.edu\/papers\/sigurbjarnarson-nickel.pdf"},{"key":"e_1_3_2_1_39_1","volume-title":"Compositional CompCert. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201915)","author":"Stewart Gordon","unstructured":"Gordon Stewart , Lennart Beringer , Santiago Cuellar , and Andrew W. Appel . 2015 . Compositional CompCert. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201915) . Association for Computing Machinery, Mumbai, India. 275\u2013287. isbn:978-1-4503-3300-9 https:\/\/www.cs.princeton.edu\/~appel\/papers\/compcomp.pdf 10.1145\/2676726.2676985. Gordon Stewart, Lennart Beringer, Santiago Cuellar, and Andrew W. Appel. 2015. Compositional CompCert. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201915). Association for Computing Machinery, Mumbai, India. 275\u2013287. isbn:978-1-4503-3300-9 https:\/\/www.cs.princeton.edu\/~appel\/papers\/compcomp.pdf 10.1145\/2676726.2676985."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290375"},{"key":"e_1_3_2_1_42_1","unstructured":"Andrew Waterman and Krste Asanovic. 2019. The RISC-V Instruction Set Manual. https:\/\/riscv.org\/specifications\/  Andrew Waterman and Krste Asanovic. 2019. The RISC-V Instruction Set Manual. https:\/\/riscv.org\/specifications\/"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359647"}],"event":{"name":"PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation","location":"Virtual Canada","acronym":"PLDI '21","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3453483.3454065","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3453483.3454065","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:47:47Z","timestamp":1750193267000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3453483.3454065"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6,18]]},"references-count":42,"alternative-id":["10.1145\/3453483.3454065","10.1145\/3453483"],"URL":"https:\/\/doi.org\/10.1145\/3453483.3454065","relation":{},"subject":[],"published":{"date-parts":[[2021,6,18]]},"assertion":[{"value":"2021-06-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}