{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,28]],"date-time":"2026-09-28T21:41:20Z","timestamp":1790631680558,"version":"4.1.0"},"publisher-location":"New York, NY, USA","reference-count":46,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,6,11]],"date-time":"2018-06-11T00:00:00Z","timestamp":1528675200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-12-2-0291"],"award-info":[{"award-number":["FA8750-12-2-0291"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CNS-1054246"],"award-info":[{"award-number":["CNS-1054246"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"name":"AFOSR","award":["FA9550-16-1-0288"],"award-info":[{"award-number":["FA9550-16-1-0288"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,6,11]]},"DOI":"10.1145\/3192366.3192406","type":"proceedings-article","created":{"date-parts":[[2018,6,12]],"date-time":"2018-06-12T08:16:01Z","timestamp":1528791361000},"page":"617-630","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":46,"title":["VeriPhy: verified controller executables from verified cyber-physical system models"],"prefix":"10.1145","author":[{"given":"Rose","family":"Bohrer","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yong Kiam","family":"Tan","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Stefan","family":"Mitsch","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Magnus O.","family":"Myreen","sequence":"additional","affiliation":[{"name":"Chalmers University of Technology, Sweden"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andr\u00e9","family":"Platzer","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2018,6,11]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Knepper","author":"Anand Abhishek","year":"2015","unstructured":"Abhishek Anand and Ross A . Knepper . 2015 . ROSCoq: Robots powered by constructive reals. In ITP (LNCS), Christian Urban and Xingyuan Zhang (Eds.), Vol. 9236 . Springer , 34-50. Abhishek Anand and Ross A. Knepper. 2015. ROSCoq: Robots powered by constructive reals. In ITP (LNCS), Christian Urban and Xingyuan Zhang (Eds.), Vol. 9236. Springer, 34-50."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018616"},{"key":"e_1_3_2_1_3_1","volume-title":"MKM, Held as Part of CICM (LNCS), Jacques Carette, Lucas Dixon, Claudio Sacerdoti Coen, and Stephen M","author":"Boldo Sylvie","unstructured":"Sylvie Boldo , Jean-Christophe Filliatre , and Guillaume Melquiond . 2009. Combining Coq and Gappa for certifying floating-point programs . In MKM, Held as Part of CICM (LNCS), Jacques Carette, Lucas Dixon, Claudio Sacerdoti Coen, and Stephen M . Watt (Eds.), Vol. 5625 . Springer , 59-74. Sylvie Boldo, Jean-Christophe Filliatre, and Guillaume Melquiond. 2009. Combining Coq and Gappa for certifying floating-point programs. In MKM, Held as Part of CICM (LNCS), Jacques Carette, Lucas Dixon, Claudio Sacerdoti Coen, and Stephen M. Watt (Eds.), Vol. 5625. Springer, 59-74."},{"key":"e_1_3_2_1_4_1","volume-title":"A formally-verified C compiler supporting floatingpoint arithmetic","author":"Boldo Sylvie","unstructured":"Sylvie Boldo , Jacques-Henri Jourdan , Xavier Leroy , and Guillaume Melquiond . 2013. A formally-verified C compiler supporting floatingpoint arithmetic . In ARITH, Alberto Nannarelli, Peter-Michael Seidel, and Ping Tak Peter Tang (Eds.). IEEE Computer Society , 107-115. Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond. 2013. A formally-verified C compiler supporting floatingpoint arithmetic. In ARITH, Alberto Nannarelli, Peter-Michael Seidel, and Ping Tak Peter Tang (Eds.). IEEE Computer Society, 107-115."},{"key":"e_1_3_2_1_5_1","volume-title":"Flocq: A unified library for proving floating-point algorithms in Coq","author":"Boldo Sylvie","year":"2011","unstructured":"Sylvie Boldo and Guillaume Melquiond . 2011 . Flocq: A unified library for proving floating-point algorithms in Coq . In ARITH, Elisardo Antelo, David Hough, and Paolo Ienne (Eds.). IEEE Computer Society , 243-252. Sylvie Boldo and Guillaume Melquiond. 2011. Flocq: A unified library for proving floating-point algorithms in Coq. In ARITH, Elisardo Antelo, David Hough, and Paolo Ienne (Eds.). IEEE Computer Society, 243-252."},{"key":"e_1_3_2_1_6_1","volume-title":"HybridFluctuat: A static analyzer of numerical programs within a continuous environment (LNCS)","author":"Bouissou Olivier","unstructured":"Olivier Bouissou , Eric Goubault , Sylvie Putot , Karim Tekkal , and Franck Vedrine . 2009. HybridFluctuat: A static analyzer of numerical programs within a continuous environment (LNCS) , Ahmed Bouajjani and Oded Maler (Eds.), Vol. 5643 . Springer , 620s626. Olivier Bouissou, Eric Goubault, Sylvie Putot, Karim Tekkal, and Franck Vedrine. 2009. HybridFluctuat: A static analyzer of numerical programs within a continuous environment (LNCS), Ahmed Bouajjani and Oded Maler (Eds.), Vol. 5643. Springer, 620s626."},{"key":"e_1_3_2_1_7_1","first-page":"586","article-title":"A formally verified compiler for Lustre. In PLDI, Albert Cohen and Martin T. Vechev (Eds.)","author":"Bourke Timothy","year":"2017","unstructured":"Timothy Bourke , Lelio Brun , Pierre-Evariste Dagand , Xavier Leroy , Marc Pouzet , and Lionel Rieg . 2017 . A formally verified compiler for Lustre. In PLDI, Albert Cohen and Martin T. Vechev (Eds.) . ACM , 586 - 601 . Timothy Bourke, Lelio Brun, Pierre-Evariste Dagand, Xavier Leroy, Marc Pouzet, and Lionel Rieg. 2017. A formally verified compiler for Lustre. In PLDI, Albert Cohen and Martin T. Vechev (Eds.). ACM, 586-601.","journal-title":"ACM"},{"key":"e_1_3_2_1_8_1","volume-title":"CAV (LNCS)","author":"Chen Xin","unstructured":"Xin Chen , Erika Abraham , and Sriram Sankaranarayanan . 2013. Flow*: An analyzer for non-linear hybrid systems . In CAV (LNCS) , Natasha Sharygina and Helmut Veith (Eds.), Vol. 8044 . Springer , 258-263. Xin Chen, Erika Abraham, and Sriram Sankaranarayanan. 2013. Flow*: An analyzer for non-linear hybrid systems. In CAV (LNCS), Natasha Sharygina and Helmut Veith (Eds.), Vol. 8044. Springer, 258-263."},{"key":"e_1_3_2_1_9_1","volume-title":"TPHOLs (LNCS), Richard J","author":"Daumas Marc","unstructured":"Marc Daumas , Laurence Rideau , and Laurent Thery . 2001. A generic library for floating-point numbers and its application to exact computing . In TPHOLs (LNCS), Richard J . Boulton and Paul B. Jackson (Eds.), Vol. 2152 . Springer , 169-184. Marc Daumas, Laurence Rideau, and Laurent Thery. 2001. A generic library for floating-point numbers and its application to exact computing. In TPHOLs (LNCS), Richard J. Boulton and Paul B. Jackson (Eds.), Vol. 2152. Springer, 169-184."},{"key":"e_1_3_2_1_10_1","volume-title":"TACAS (LNCS)","author":"Duggirala Parasara Sridhar","unstructured":"Parasara Sridhar Duggirala , Sayan Mitra , Mahesh Viswanathan , and Matthew Potok . 2015. C2E2: A verification tool for stateflow models . In TACAS (LNCS) , Christel Baier and Cesare Tinelli (Eds.), Vol. 9035 . Springer , 68-82. Parasara Sridhar Duggirala, Sayan Mitra, Mahesh Viswanathan, and Matthew Potok. 2015. C2E2: A verification tool for stateflow models. In TACAS (LNCS), Christel Baier and Cesare Tinelli (Eds.), Vol. 9035. Springer, 68-82."},{"key":"e_1_3_2_1_11_1","first-page":"189","article-title":"Guilt free ivory","author":"Elliott Trevor","year":"2015","unstructured":"Trevor Elliott , Lee Pike , Simon Winwood , Patrick C. Hickey , James Bielman , Jamey Sharp , Eric L. Seidel , and John Launchbury . 2015 . Guilt free ivory . In Haskell. 189 - 200 . Trevor Elliott, Lee Pike, Simon Winwood, Patrick C. Hickey, James Bielman, Jamey Sharp, Eric L. Seidel, and John Launchbury. 2015. Guilt free ivory. In Haskell. 189-200.","journal-title":"Haskell."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/MCS.2016.2643244"},{"key":"e_1_3_2_1_13_1","volume-title":"Alexandre Donze, Scott Cotton, Rajarshi Ray, Olivier Lebeltel, Rodolfo Ripado, Antoine Girard, Thao Dang, and Oded Maler.","author":"Frehse Goran","year":"2011","unstructured":"Goran Frehse , Colas Le Guernic , Alexandre Donze, Scott Cotton, Rajarshi Ray, Olivier Lebeltel, Rodolfo Ripado, Antoine Girard, Thao Dang, and Oded Maler. 2011 . SpaceEx: Scalable verification of hybrid systems. In CAV (LNCS), Ganesh Gopalakrishnan and Shaz Qadeer (Eds .), Vol. 6806 . 379-395. Goran Frehse, Colas Le Guernic, Alexandre Donze, Scott Cotton, Rajarshi Ray, Olivier Lebeltel, Rodolfo Ripado, Antoine Girard, Thao Dang, and Oded Maler. 2011. SpaceEx: Scalable verification of hybrid systems. In CAV (LNCS), Ganesh Gopalakrishnan and Shaz Qadeer (Eds.), Vol. 6806. 379-395."},{"key":"e_1_3_2_1_14_1","volume-title":"Bellerophon: Tactical theorem proving for hybrid systems. In ITP (LNCS), Mauricio Ayala-Rincon and Cesar A","author":"Fulton Nathan","year":"2017","unstructured":"Nathan Fulton , Stefan Mitsch , Rose Bohrer , and Andre Platzer . 2017 . Bellerophon: Tactical theorem proving for hybrid systems. In ITP (LNCS), Mauricio Ayala-Rincon and Cesar A . Munoz (Eds.), Vol. 10499 . Springer , 207-224. Nathan Fulton, Stefan Mitsch, Rose Bohrer, and Andre Platzer. 2017. Bellerophon: Tactical theorem proving for hybrid systems. In ITP (LNCS), Mauricio Ayala-Rincon and Cesar A. Munoz (Eds.), Vol. 10499. Springer, 207-224."},{"key":"e_1_3_2_1_15_1","volume-title":"CADE (LNCS)","author":"Fulton Nathan","unstructured":"Nathan Fulton , Stefan Mitsch , Jan-David Quesel , Marcus Volp , and Andre Platzer . 2015. KeYmaera X: An axiomatic tactical theorem prover for hybrid systems . In CADE (LNCS) , Amy Felty and Aart Middeldorp (Eds.), Vol. 9195 . Springer , 527-538. Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Volp, and Andre Platzer. 2015. KeYmaera X: An axiomatic tactical theorem prover for hybrid systems. In CADE (LNCS), Amy Felty and Aart Middeldorp (Eds.), Vol. 9195. Springer, 527-538."},{"key":"e_1_3_2_1_16_1","volume-title":"ESOP (LNCS)","author":"Gueneau Armael","unstructured":"Armael Gueneau , Magnus O. Myreen , Ramana Kumar , and Michael Norrish . 2017. Verified characteristic formulae for CakeML . In ESOP (LNCS) , Hongseok Yang (Ed.), Vol. 10201 . Springer , 584-610. Armael Gueneau, Magnus O. Myreen, Ramana Kumar, and Michael Norrish. 2017. Verified characteristic formulae for CakeML. In ESOP (LNCS), Hongseok Yang (Ed.), Vol. 10201. Springer, 584-610."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.159839"},{"key":"e_1_3_2_1_18_1","volume-title":"Formal Methods for Hardware Verification, SFM (LNCS)","author":"Harrison John","unstructured":"John Harrison . 2006. Floating-point verification using theorem proving . In Formal Methods for Hardware Verification, SFM (LNCS) , Marco Bernardo and Alessandro Cimatti (Eds.), Vol. 3965 . Springer , 211-242. John Harrison. 2006. Floating-point verification using theorem proving. In Formal Methods for Hardware Verification, SFM (LNCS), Marco Bernardo and Alessandro Cimatti (Eds.), Vol. 3965. Springer, 211-242."},{"key":"e_1_3_2_1_19_1","volume-title":"TPHOLs (LNCS)","author":"Harrison John","unstructured":"John Harrison . 2007. Verifying nonlinear real formulas via sums of squares . In TPHOLs (LNCS) , Klaus Schneider and Jens Brandt (Eds.), Vol. 4732 . Springer , 102-118. John Harrison. 2007. Verifying nonlinear real formulas via sums of squares. In TPHOLs (LNCS), Klaus Schneider and Jens Brandt (Eds.), Vol. 4732. Springer, 102-118."},{"key":"e_1_3_2_1_20_1","first-page":"278","article-title":"The theory of hybrid automata","author":"Henzinger Thomas A.","year":"1996","unstructured":"Thomas A. Henzinger . 1996 . The theory of hybrid automata . In LICS. IEEE Computer Society , 278 - 292 . Thomas A. Henzinger. 1996. The theory of hybrid automata. In LICS. IEEE Computer Society, 278-292.","journal-title":"LICS. IEEE Computer Society"},{"key":"e_1_3_2_1_21_1","volume-title":"ESOP (LNCS)","author":"Hupel Lars","unstructured":"Lars Hupel and Tobias Nipkow . 2018. A Verified Compiler from Isabelle\/ HOL to CakeML . In ESOP (LNCS) , Amal Ahmed (Ed.). Springer . Lars Hupel and Tobias Nipkow. 2018. A Verified Compiler from Isabelle\/ HOL to CakeML. In ESOP (LNCS), Amal Ahmed (Ed.). Springer."},{"key":"e_1_3_2_1_22_1","volume-title":"NFM (LNCS), Mihaela Gheorghiu Bobaru, Klaus Havelund, Gerard J","author":"Hurd Joe","unstructured":"Joe Hurd . 2011. The OpenTheory standard theory library . In NFM (LNCS), Mihaela Gheorghiu Bobaru, Klaus Havelund, Gerard J . Holzmann, and Rajeev Joshi (Eds.), Vol. 6617 . Springer , 177-191. Joe Hurd. 2011. The OpenTheory standard theory library. In NFM (LNCS), Mihaela Gheorghiu Bobaru, Klaus Havelund, Gerard J. Holzmann, and Rajeev Joshi (Eds.), Vol. 6617. Springer, 177-191."},{"key":"e_1_3_2_1_23_1","volume-title":"ITP (LNCS)","author":"Immler Fabian","unstructured":"Fabian Immler and Christoph Traut . 2016. The flow of ODEs . In ITP (LNCS) , Jasmin Christian Blanchette and Stephan Merz (Eds.), Vol. 9807 . Springer , 184-199. Fabian Immler and Christoph Traut. 2016. The flow of ODEs. In ITP (LNCS), Jasmin Christian Blanchette and Stephan Merz (Eds.), Vol. 9807. Springer, 184-199."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1743546.1743574"},{"key":"e_1_3_2_1_25_1","first-page":"179","article-title":"CakeML: A verified implementation of ML. In POPL, Suresh Jagannathan and Peter Sewell (Eds.)","author":"Kumar Ramana","year":"2014","unstructured":"Ramana Kumar , Magnus O. Myreen , Michael Norrish , and Scott Owens . 2014 . CakeML: A verified implementation of ML. In POPL, Suresh Jagannathan and Peter Sewell (Eds.) . ACM , 179 - 192 . Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. 2014. CakeML: A verified implementation of ML. In POPL, Suresh Jagannathan and Peter Sewell (Eds.). ACM, 179-192.","journal-title":"ACM"},{"key":"e_1_3_2_1_26_1","first-page":"123","article-title":"Synthesis of minimal-error control software. In EMSOFT, Ahmed Jerraya, Luca P. Carloni, Florence Maraninchi, and John Regehr (Eds.)","author":"Majumdar Rupak","year":"2012","unstructured":"Rupak Majumdar , Indranil Saha , and Majid Zamani . 2012 . Synthesis of minimal-error control software. In EMSOFT, Ahmed Jerraya, Luca P. Carloni, Florence Maraninchi, and John Regehr (Eds.) . ACM , 123 - 132 . Rupak Majumdar, Indranil Saha, and Majid Zamani. 2012. Synthesis of minimal-error control software. In EMSOFT, Ahmed Jerraya, Luca P. Carloni, Florence Maraninchi, and John Regehr (Eds.). ACM, 123-132.","journal-title":"ACM"},{"key":"e_1_3_2_1_27_1","first-page":"1","article-title":"Towards foundational verification of cyber-physical systems. In SOSCYPS@CPSWeek","author":"Malecha Gregory","year":"2016","unstructured":"Gregory Malecha , Daniel Ricketts , Mario M. Alvarez , and Sorin Lerner . 2016 . Towards foundational verification of cyber-physical systems. In SOSCYPS@CPSWeek . IEEE Computer Society , 1 - 5 . Gregory Malecha, Daniel Ricketts, Mario M. Alvarez, and Sorin Lerner. 2016. Towards foundational verification of cyber-physical systems. In SOSCYPS@CPSWeek. IEEE Computer Society, 1-5.","journal-title":"IEEE Computer Society"},{"key":"e_1_3_2_1_28_1","first-page":"9","article-title":"Automatic verification of control system implementations. In EMSOFT, Luca P. Carloni and Stavros Tripakis (Eds.)","author":"Martinez Adolfo Anta","year":"2010","unstructured":"Adolfo Anta Martinez , Rupak Majumdar , Indranil Saha , and Paulo Tabuada . 2010 . Automatic verification of control system implementations. In EMSOFT, Luca P. Carloni and Stavros Tripakis (Eds.) . ACM , 9 - 8 . Adolfo Anta Martinez, Rupak Majumdar, Indranil Saha, and Paulo Tabuada. 2010. Automatic verification of control system implementations. In EMSOFT, Luca P. Carloni and Stavros Tripakis (Eds.). ACM, 9-8.","journal-title":"ACM"},{"key":"e_1_3_2_1_29_1","volume-title":"CADE (LNCS)","author":"McLaughlin Sean","unstructured":"Sean McLaughlin and John Harrison . 2005. A proof-producing decision procedure for real arithmetic . In CADE (LNCS) , Robert Nieuwenhuis (Ed.), Vol. 3632 . Springer , 295-314. Sean McLaughlin and John Harrison. 2005. A proof-producing decision procedure for real arithmetic. In CADE (LNCS), Robert Nieuwenhuis (Ed.), Vol. 3632. Springer, 295-314."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2011.09.005"},{"key":"e_1_3_2_1_31_1","first-page":"67","volume-title":"3rd Workshop on Formal Integrated Development Environment (EPTCS), Catherine Dubois, Dominique Mery, and Paolo Masci (Eds.)","volume":"240","author":"Mitsch Stefan","year":"2016","unstructured":"Stefan Mitsch and Andre Platzer . 2016 . The KeYmaera X proof IDE: Concepts on usability in hybrid systems theorem proving . In 3rd Workshop on Formal Integrated Development Environment (EPTCS), Catherine Dubois, Dominique Mery, and Paolo Masci (Eds.) , Vol. 240 . Open Publishing Association , 67 - 81 . Stefan Mitsch and Andre Platzer. 2016. The KeYmaera X proof IDE: Concepts on usability in hybrid systems theorem proving. In 3rd Workshop on Formal Integrated Development Environment (EPTCS), Catherine Dubois, Dominique Mery, and Paolo Masci (Eds.), Vol. 240. Open Publishing Association, 67-81."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0241-z"},{"key":"e_1_3_2_1_33_1","volume-title":"ITP (LNCS), Marko C","author":"Monniaux David","unstructured":"David Monniaux and Pierre Corbineau . 2011. On the generation of Positivstellensatz witnesses in degenerate cases . In ITP (LNCS), Marko C . J. D. van Eekelen, Herman Geuvers, Julien Schmaltz, and Freek Wiedijk (Eds.), Vol. 6898 . Springer , 249-264. David Monniaux and Pierre Corbineau. 2011. On the generation of Positivstellensatz witnesses in degenerate cases. In ITP (LNCS), Marko C. J. D. van Eekelen, Herman Geuvers, Julien Schmaltz, and Freek Wiedijk (Eds.), Vol. 6898. Springer, 249-264."},{"key":"e_1_3_2_1_34_1","first-page":"395","article-title":"RockSalt: better, faster, stronger SFI for the x86. In PLDI, Jan Vitek, Haibo Lin, and Frank Tip (Eds.)","author":"Morrisett Greg","year":"2012","unstructured":"Greg Morrisett , Gang Tan , Joseph Tassarotti , Jean-Baptiste Tristan , and Edward Gan . 2012 . RockSalt: better, faster, stronger SFI for the x86. In PLDI, Jan Vitek, Haibo Lin, and Frank Tip (Eds.) . ACM , 395 - 404 . Greg Morrisett, Gang Tan, Joseph Tassarotti, Jean-Baptiste Tristan, and Edward Gan. 2012. RockSalt: better, faster, stronger SFI for the x86. In PLDI, Jan Vitek, Haibo Lin, and Frank Tip (Eds.). ACM, 395-404.","journal-title":"ACM"},{"key":"e_1_3_2_1_35_1","volume-title":"Myreen and Scott Owens","author":"Magnus","year":"2012","unstructured":"Magnus O. Myreen and Scott Owens . 2012 . Proof-producing synthesis of ML from higher-order logic. In ICFP, Peter Thiemann and Robby Bruce Findler (Eds.). ACM , 115-126. Magnus O. Myreen and Scott Owens. 2012. Proof-producing synthesis of ML from higher-order logic. In ICFP, Peter Thiemann and Robby Bruce Findler (Eds.). ACM, 115-126."},{"key":"e_1_3_2_1_36_1","first-page":"1","article-title":"Programming languages for high-assurance autonomous vehicles: Extended abstract","author":"Pike Lee","year":"2014","unstructured":"Lee Pike , Patrick C. Hickey , James Bielman , Trevor Elliott , Thomas DuBuisson , and John Launchbury . 2014 . Programming languages for high-assurance autonomous vehicles: Extended abstract . In PLPV. 1 - 2 . Lee Pike, Patrick C. Hickey, James Bielman, Trevor Elliott, Thomas DuBuisson, and John Launchbury. 2014. Programming languages for high-assurance autonomous vehicles: Extended abstract. In PLPV. 1-2.","journal-title":"PLPV."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9103-8"},{"key":"e_1_3_2_1_38_1","volume-title":"Logics of dynamical systems","author":"Platzer Andre","unstructured":"Andre Platzer . 2012. Logics of dynamical systems . In LICS. IEEE Computer Society , 13s24. Andre Platzer. 2012. Logics of dynamical systems. In LICS. IEEE Computer Society, 13s24."},{"key":"e_1_3_2_1_39_1","volume-title":"IJCAR (LNCS)","author":"Platzer Andre","unstructured":"Andre Platzer . 2016. Logic & proofs for cyber-physical systems . In IJCAR (LNCS) , Nicola Olivetti and Ashish Tiwari (Eds.), Vol. 9706 . Springer , 15-21. Andre Platzer. 2016. Logic & proofs for cyber-physical systems. In IJCAR (LNCS), Nicola Olivetti and Ashish Tiwari (Eds.), Vol. 9706. Springer, 15-21."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9385-1"},{"key":"e_1_3_2_1_41_1","volume-title":"ICFEM (LNCS)","author":"Platzer Andre","unstructured":"Andre Platzer and Jan-David Quesel . 2009. European Train Control System: A case study in formal verification . In ICFEM (LNCS) , Karin Breitman and Ana Cavalcanti (Eds.), Vol. 5885 . Springer , 246-265. Andre Platzer and Jan-David Quesel. 2009. European Train Control System: A case study in formal verification. In ICFEM (LNCS), Karin Breitman and Ana Cavalcanti (Eds.), Vol. 5885. Springer, 246-265."},{"key":"e_1_3_2_1_42_1","volume-title":"CADE (LNCS), Renate A","author":"Platzer Andre","unstructured":"Andre Platzer , Jan-David Quesel , and Philipp Rummer . 2009. Real world verification . In CADE (LNCS), Renate A . Schmidt (Ed.), Vol. 5663 . Springer , 485-501. Andre Platzer, Jan-David Quesel, and Philipp Rummer. 2009. Real world verification. In CADE (LNCS), Renate A. Schmidt (Ed.), Vol. 5663. Springer, 485-501."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0367-0"},{"key":"e_1_3_2_1_44_1","first-page":"471","article-title":"Translation validation for a verified OS kernel. In PLDI, Hans-Juergen Boehm and Cormac Flanagan (Eds.)","author":"Leck Sewell Thomas Arthur","year":"2013","unstructured":"Thomas Arthur Leck Sewell , Magnus O. Myreen , and Gerwin Klein . 2013 . Translation validation for a verified OS kernel. In PLDI, Hans-Juergen Boehm and Cormac Flanagan (Eds.) . ACM , 471 - 482 . Thomas Arthur Leck Sewell, Magnus O. Myreen, and Gerwin Klein. 2013. Translation validation for a verified OS kernel. In PLDI, Hans-Juergen Boehm and Cormac Flanagan (Eds.). ACM, 471-482.","journal-title":"ACM"},{"key":"e_1_3_2_1_45_1","first-page":"60","article-title":"A new verified compiler backend for CakeML. In ICFP, Jacques Garrigue, Gabriele Keller, and Eijiro Sumii (Eds.)","author":"Tan Yong Kiam","year":"2016","unstructured":"Yong Kiam Tan , Magnus O. Myreen , Ramana Kumar , Anthony C. J. Fox , Scott Owens , and Michael Norrish . 2016 . A new verified compiler backend for CakeML. In ICFP, Jacques Garrigue, Gabriele Keller, and Eijiro Sumii (Eds.) . ACM , 60 - 73 . Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens, and Michael Norrish. 2016. A new verified compiler backend for CakeML. In ICFP, Jacques Garrigue, Gabriele Keller, and Eijiro Sumii (Eds.). ACM, 60-73.","journal-title":"ACM"},{"key":"e_1_3_2_1_46_1","volume-title":"A formal model of IEEE floating point arithmetic. Archive of Formal Proofs","author":"Lei Yu.","year":"2013","unstructured":"Lei Yu. 2013. A formal model of IEEE floating point arithmetic. Archive of Formal Proofs ( 2013 ). https:\/\/www.isa-afp.org\/entries\/IEEE_Floating_Point.shtml Lei Yu. 2013. A formal model of IEEE floating point arithmetic. Archive of Formal Proofs (2013). https:\/\/www.isa-afp.org\/entries\/IEEE_Floating_Point.shtml"}],"event":{"name":"PLDI '18: ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Philadelphia PA USA","acronym":"PLDI '18","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3192366.3192406","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3192366.3192406","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3192366.3192406","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:07:53Z","timestamp":1750198073000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3192366.3192406"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,6,11]]},"references-count":46,"alternative-id":["10.1145\/3192366.3192406","10.1145\/3192366"],"URL":"https:\/\/doi.org\/10.1145\/3192366.3192406","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3296979.3192406","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2018,6,11]]},"assertion":[{"value":"2018-06-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}