{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,14]],"date-time":"2026-03-14T17:59:00Z","timestamp":1773511140138,"version":"3.50.1"},"reference-count":61,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2021,6,1]],"date-time":"2021-06-01T00:00:00Z","timestamp":1622505600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-18-1-2020"],"award-info":[{"award-number":["N00014-18-1-2020"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-1930041,CNS-1544678,CNS-1850533,CNS-1929771"],"award-info":[{"award-number":["CNS-1930041,CNS-1544678,CNS-1850533,CNS-1929771"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Meas. Anal. Comput. Syst."],"published-print":{"date-parts":[[2021,6]]},"abstract":"<jats:p>Safety compliance is paramount to the safe deployment of autonomous vehicle (AV) technologies in real-world transportation systems. As AVs will share road infrastructures with human drivers and pedestrians, it is an important requirement for AVs to obey standard driving rules. Existing AV software testing methods, including simulation and road testing, only check fundamental safety rules such as collision avoidance and safety distance. Scenario-dependent driving rules, including crosswalk and intersection rules, are more complicated because the expected driving behavior heavily depends on the surrounding circumstances. However, a testing framework is missing for checking scenario-dependent driving rules on various AV software.<\/jats:p>\n          <jats:p>In this paper, we design and implement a systematic framework AVChecker for identifying violations of scenario-dependent driving rules in AV software using formal methods. AVChecker represents both the code logic of AV software and driving rules in proposed formal specifications and leverages satisfiability modulo theory (SMT) solvers to identify driving rule violations. To improve the automation of systematic rule-based checking, AVChecker provides a powerful user interface for writing driving rule specifications and applies static code analysis to extract rule-related code logic from the AV software codebase. Evaluations on two open-source AV software platforms, Baidu Apollo and Autoware, uncover 19 true violations out of 28 real-world driving rules covering crosswalks, traffic lights, stop signs, and intersections. Seven of the violations can lead to severe risks of a collision with pedestrians or blocking traffic.<\/jats:p>","DOI":"10.1145\/3460082","type":"journal-article","created":{"date-parts":[[2021,6,4]],"date-time":"2021-06-04T14:44:15Z","timestamp":1622817855000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["A Systematic Framework to Identify Violations of Scenario-dependent Driving Rules in Autonomous Vehicle Software"],"prefix":"10.1145","volume":"5","author":[{"given":"Qingzhao","family":"Zhang","sequence":"first","affiliation":[{"name":"University of Michigan, Ann Arbor, MI, USA"}]},{"given":"David Ke","family":"Hong","sequence":"additional","affiliation":[{"name":"University of Michigan, Ann Arbor, MI, USA"}]},{"given":"Ze","family":"Zhang","sequence":"additional","affiliation":[{"name":"University of Michigan, Ann Arbor, MI, USA"}]},{"given":"Qi Alfred","family":"Chen","sequence":"additional","affiliation":[{"name":"University of California, Irvine, Irvine, CA, USA"}]},{"given":"Scott","family":"Mahlke","sequence":"additional","affiliation":[{"name":"University of Michigan, Ann Arbor, MI, USA"}]},{"given":"Z. Morley","family":"Mao","sequence":"additional","affiliation":[{"name":"University of Michigan, Ann Arbor, MI, USA"}]}],"member":"320","published-online":{"date-parts":[[2021,6,4]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"2017. Automated Driving Systems 2.0: A Vision for Safety. https:\/\/www.nhtsa.gov\/sites\/nhtsa.dot.gov\/files\/documents\/13069a-ads2.0_090617_v9a_tag.pdf.  2017. Automated Driving Systems 2.0: A Vision for Safety. https:\/\/www.nhtsa.gov\/sites\/nhtsa.dot.gov\/files\/documents\/13069a-ads2.0_090617_v9a_tag.pdf."},{"key":"e_1_2_1_2_1","unstructured":"2019. A Matter of Trust Ford's Approach to Developing Self-driving Vehicles. https:\/\/media.ford.com\/content\/dam\/fordmedia\/pdf\/Ford_AV_LLC_FINAL_HR_2.pdf.  2019. A Matter of Trust Ford's Approach to Developing Self-driving Vehicles. https:\/\/media.ford.com\/content\/dam\/fordmedia\/pdf\/Ford_AV_LLC_FINAL_HR_2.pdf."},{"key":"e_1_2_1_3_1","unstructured":"2019. Apollo Auto: An open autonomous driving platform. https:\/\/github.com\/ApolloAuto\/apollo.  2019. Apollo Auto: An open autonomous driving platform. https:\/\/github.com\/ApolloAuto\/apollo."},{"key":"e_1_2_1_4_1","unstructured":"2019. General Motors 2018 Self-Driving Safety Report. https:\/\/www.gm.com\/content\/dam\/company\/docs\/us\/en\/gmcom\/gmsafetyreport.pdf .  2019. General Motors 2018 Self-Driving Safety Report. https:\/\/www.gm.com\/content\/dam\/company\/docs\/us\/en\/gmcom\/gmsafetyreport.pdf ."},{"key":"e_1_2_1_5_1","unstructured":"2020. 2010 Georgia Code Title 40 - Motor Vehicles and Traffic. https:\/\/law.justia.com\/codes\/georgia\/2010\/title-40\/chapter-6\/article-5\/40--6--91.  2020. 2010 Georgia Code Title 40 - Motor Vehicles and Traffic. https:\/\/law.justia.com\/codes\/georgia\/2010\/title-40\/chapter-6\/article-5\/40--6--91."},{"key":"e_1_2_1_6_1","unstructured":"2020. Autoware: Open-source software for self-driving vehicles. https:\/\/gitlab.com\/autowarefoundation\/autoware.ai.  2020. Autoware: Open-source software for self-driving vehicles. https:\/\/gitlab.com\/autowarefoundation\/autoware.ai."},{"key":"e_1_2_1_7_1","unstructured":"2020. Baidu Apollo's fuzzing support. https:\/\/github.com\/ApolloAuto\/apollo\/commit\/7aca63966211ceada44981d96b35a1252f9f1729.  2020. Baidu Apollo's fuzzing support. https:\/\/github.com\/ApolloAuto\/apollo\/commit\/7aca63966211ceada44981d96b35a1252f9f1729."},{"key":"e_1_2_1_8_1","unstructured":"2020. Louisiana DMV Handbook. https:\/\/driving-tests.org\/wp-content\/uploads\/2018\/03\/LA_Guide-2017.pdf .  2020. Louisiana DMV Handbook. https:\/\/driving-tests.org\/wp-content\/uploads\/2018\/03\/LA_Guide-2017.pdf ."},{"key":"e_1_2_1_9_1","unstructured":"2020. New York State DMV: Driver's Manual and Practice Tests. https:\/\/dmv.ny.gov\/driver-license\/drivers-manual-practice-tests.  2020. New York State DMV: Driver's Manual and Practice Tests. https:\/\/dmv.ny.gov\/driver-license\/drivers-manual-practice-tests."},{"key":"e_1_2_1_10_1","unstructured":"2020. ROS.org | Powering the world's robots. https:\/\/www.ros.org\/.  2020. ROS.org | Powering the world's robots. https:\/\/www.ros.org\/."},{"key":"e_1_2_1_11_1","unstructured":"2020. State of California DMV: California Driver Handbook. https:\/\/www.dmv.ca.gov\/web\/eng_pdf\/dl600.pdf.  2020. State of California DMV: California Driver Handbook. https:\/\/www.dmv.ca.gov\/web\/eng_pdf\/dl600.pdf."},{"key":"e_1_2_1_12_1","unstructured":"2020. State of Michigan DMV: What Every Driver Must Know. https:\/\/www.michigan.gov\/documents\/wedmk_16312_7.pdf.  2020. State of Michigan DMV: What Every Driver Must Know. https:\/\/www.michigan.gov\/documents\/wedmk_16312_7.pdf."},{"key":"e_1_2_1_13_1","unstructured":"2020. Waymo Safety Report. https:\/\/waymo.com\/safety.  2020. Waymo Safety Report. https:\/\/waymo.com\/safety."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/ITSC.2011.6083052"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/IVS.2018.8500374"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/TITS.2009.2018966"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/LRA.2020.2966414"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/IVS.2019.8813793"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48869-1_14"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9432-6"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_27"},{"key":"e_1_2_1_22_1","unstructured":"NTS Board. 2018. Preliminary report highway hwy18mh010.National Transpotation Safety Board https:\/\/www.ntsb.gov\/investigations\/AccidentReports\/Reports\/HWY18MH010-prelim.pdf accessed(2018) 11--15.  NTS Board. 2018. Preliminary report highway hwy18mh010.National Transpotation Safety Board https:\/\/www.ntsb.gov\/investigations\/AccidentReports\/Reports\/HWY18MH010-prelim.pdf accessed(2018) 11--15."},{"key":"e_1_2_1_23_1","volume-title":"KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In 8th USENIX Symposium on Operating Systems Design and Implementation(OSDI 08)","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar , Daniel Dunbar , and Dawson Engler . 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 08) . 209--224. Cristian Cadar, Daniel Dunbar, and Dawson Engler. 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 08). 209--224."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2659787.2659812"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_26_1","volume-title":"CARLA: An open urban driving simulator. arXiv preprint arXiv:1711.03938(2017).","author":"Dosovitskiy Alexey","year":"2017","unstructured":"Alexey Dosovitskiy , German Ros , Felipe Codevilla , Antonio Lopez , and Vladlen Koltun . 2017 . CARLA: An open urban driving simulator. arXiv preprint arXiv:1711.03938(2017). Alexey Dosovitskiy, German Ros, Felipe Codevilla, Antonio Lopez, and Vladlen Koltun. 2017. CARLA: An open urban driving simulator. arXiv preprint arXiv:1711.03938(2017)."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_5"},{"key":"e_1_2_1_28_1","unstructured":"Haoyang Fan Fan Zhu Changchun Liu Liangliang Zhang Li Zhuang Dong Li Weicheng Zhu Jiangtao Hu Hongye Li and Qi Kong. 2018. Baidu apollo em motion planner.arXiv preprint arXiv:1807.08048(2018).  Haoyang Fan Fan Zhu Changchun Liu Liangliang Zhang Li Zhuang Dong Li Weicheng Zhu Jiangtao Hu Hongye Li and Qi Kong. 2018. Baidu apollo em motion planner.arXiv preprint arXiv:1807.08048(2018)."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN-W.2018.00070"},{"key":"e_1_2_1_30_1","volume-title":"Proceedings of the 2017 Workshop on Forming an Ecosystem Around Software Transformation.","author":"Hong David Ke","unstructured":"David Ke Hong , Qi Alfred Chen , and Z. Morley Mao . 2017. An Initial Investigation of Protocol Customization . In Proceedings of the 2017 Workshop on Forming an Ecosystem Around Software Transformation. David Ke Hong, Qi Alfred Chen, and Z. Morley Mao. 2017. An Initial Investigation of Protocol Customization. In Proceedings of the 2017 Workshop on Forming an Ecosystem Around Software Transformation."},{"key":"e_1_2_1_31_1","volume-title":"AVGuardian: Detecting and Mitigating Publish-Subscribe Overprivilege for Autonomous Vehicle Systems. In 2020 IEEE European Symposium on Security and Privacy (EuroS&P). 445--459","author":"Hong David Ke","year":"2020","unstructured":"David Ke Hong , John Kloosterman , Yuqi Jin , Yulong Cao , Qi Alfred Chen , Scott Mahlke , and Z Morley Mao . 2020 . AVGuardian: Detecting and Mitigating Publish-Subscribe Overprivilege for Autonomous Vehicle Systems. In 2020 IEEE European Symposium on Security and Privacy (EuroS&P). 445--459 . David Ke Hong, John Kloosterman, Yuqi Jin, Yulong Cao, Qi Alfred Chen, Scott Mahlke, and Z Morley Mao. 2020. AVGuardian: Detecting and Mitigating Publish-Subscribe Overprivilege for Autonomous Vehicle Systems. In 2020 IEEE European Symposium on Security and Privacy (EuroS&P). 445--459."},{"key":"e_1_2_1_33_1","volume-title":"Verification andReliability24, 8","author":"Jee Eunkyoung","year":"2014","unstructured":"Eunkyoung Jee , Donghwan Shin , Sungdeok Cha , Jang-Soo Lee , and Doo-Hwan Bae . 2014. Automated test case generation for FBD programs implementing reactor protection system software.Software Testing , Verification andReliability24, 8 ( 2014 ), 608--628. Eunkyoung Jee, Donghwan Shin, Sungdeok Cha, Jang-Soo Lee, and Doo-Hwan Bae. 2014. Automated test case generation for FBD programs implementing reactor protection system software.Software Testing, Verification andReliability24, 8 (2014), 608--628."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2968478.2968498"},{"key":"e_1_2_1_36_1","doi-asserted-by":"crossref","unstructured":"Philip Koopman and Michael Wagner. 2016. Challenges in autonomous vehicle testing and validation. SAE International Journal of Transportation Safety(2016).  Philip Koopman and Michael Wagner. 2016. Challenges in autonomous vehicle testing and validation. SAE International Journal of Transportation Safety(2016).","DOI":"10.4271\/2016-01-0128"},{"key":"e_1_2_1_37_1","volume-title":"Autonomous vehicle safety: An interdisciplinary challenge","author":"Koopman Philip","year":"2017","unstructured":"Philip Koopman and Michael Wagner . 2017. Autonomous vehicle safety: An interdisciplinary challenge . IEEE Intelligent Transportation Systems Magazine( 2017 ). Philip Koopman and Michael Wagner. 2017. Autonomous vehicle safety: An interdisciplinary challenge. IEEE Intelligent Transportation Systems Magazine(2017)."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2004.1281665"},{"key":"e_1_2_1_39_1","doi-asserted-by":"crossref","unstructured":"John Leonard Jonathan How Seth Teller Mitch Berger Stefan Campbell Gaston Fiore Luke Fletcher Emilio Frazzoli Albert Huang Sertac Karaman Olivier Koch Yoshiaki Kuwata David Moore Edwin Olson Steve Peters Justin Teo Robert Truax Matthew Walter David Barrett Alexander Epstein Keoni Maheloni Katy Moyer Troy Jones Ryan Buckley Matthew Antone Robert Galejs Siddhartha Krishnamurthy and Jonathan Williams. 2008. A Perception-Driven Autonomous Urban Vehicle. Journal of Field Robotic(2008).  John Leonard Jonathan How Seth Teller Mitch Berger Stefan Campbell Gaston Fiore Luke Fletcher Emilio Frazzoli Albert Huang Sertac Karaman Olivier Koch Yoshiaki Kuwata David Moore Edwin Olson Steve Peters Justin Teo Robert Truax Matthew Walter David Barrett Alexander Epstein Keoni Maheloni Katy Moyer Troy Jones Ryan Buckley Matthew Antone Robert Galejs Siddhartha Krishnamurthy and Jonathan Williams. 2008. A Perception-Driven Autonomous Urban Vehicle. Journal of Field Robotic(2008).","DOI":"10.1002\/rob.20262"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1882291.1882320"},{"key":"e_1_2_1_41_1","volume-title":"ISSRE'20","author":"Li Guanpeng","year":"2020","unstructured":"Guanpeng Li , Yiran Li , Saurabh Jha , Timothy Tsai , Siva Hari , Michael Sullivan , Zbigniew T. Kalbarczyk , and Ravis-hankar K. Iyer . 2020. AV-FUZZER: Finding safety violations in autonomous driving systems . ISSRE'20 , Proceedings of the IEEE International Conference on Software Reliability Engineering ( Nov 2020 ). Guanpeng Li, Yiran Li, Saurabh Jha, Timothy Tsai, Siva Hari, Michael Sullivan, Zbigniew T. Kalbarczyk, and Ravis-hankar K. Iyer. 2020. AV-FUZZER: Finding safety violations in autonomous driving systems. ISSRE'20, Proceedings of the IEEE International Conference on Software Reliability Engineering(Nov 2020)."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCST.2017.2723574"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1049\/iet-its.2018.5335"},{"key":"e_1_2_1_44_1","volume-title":"Junior: The Stanford Entry in the Urban Challenge. Journal of Field Robotics, Special Issue on the 2007 DARPA Urban Challenge, Part II(2008).","author":"Montemerlo M.","year":"2008","unstructured":"M. Montemerlo , J. Becker , S. Bhat , H. Dahlkamp , D. Dolgov , S. Ettinger , D. Haehnel , T. Hilden , G. Hoffmann , B. Huhnke , D. Johnston , S. Klumpp , D. Langer , A. Levandowski , J. Levinson , J. Marcil , D. Orenstein , J. Paefgen , I. Penny , A. Petrovskaya , M. Pflueger , G. Stanek , D. Stavens , A. Vogt , and S. Thrun . 2008 . Junior: The Stanford Entry in the Urban Challenge. Journal of Field Robotics, Special Issue on the 2007 DARPA Urban Challenge, Part II(2008). M. Montemerlo, J. Becker, S. Bhat, H. Dahlkamp, D. Dolgov, S. Ettinger, D. Haehnel, T. Hilden, G. Hoffmann, B.Huhnke, D. Johnston, S. Klumpp, D. Langer, A. Levandowski, J. Levinson, J. Marcil, D. Orenstein, J. Paefgen, I. Penny,A. Petrovskaya, M. Pflueger, G. Stanek, D. Stavens, A. Vogt, and S. Thrun. 2008. Junior: The Stanford Entry in the Urban Challenge. Journal of Field Robotics, Special Issue on the 2007 DARPA Urban Challenge, Part II(2008)."},{"key":"e_1_2_1_45_1","volume-title":"Proceedings of the 26th Symposium on Operating Systems Principles. 252--269","author":"Nelson Luke","unstructured":"Luke Nelson , Helgi Sigurbjarnarson , Kaiyuan Zhang , Dylan Johnson , James Bornholt , Emina Torlak , and Xi Wang .2017. Hyperkernel : Push-button verification of an OS kernel . In Proceedings of the 26th Symposium on Operating Systems Principles. 252--269 . Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dylan Johnson, James Bornholt, Emina Torlak, and Xi Wang.2017. Hyperkernel: Push-button verification of an OS kernel. In Proceedings of the 26th Symposium on Operating Systems Principles. 252--269."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3185467.3185497"},{"key":"e_1_2_1_47_1","unstructured":"Matthew O'Kelly Aman Sinha Hongseok Namkoong Russ Tedrake and John C Duchi. 2018. Scalable end-to-end autonomous vehicle testing via rare-event simulation. In Advances in Neural Information Processing Systems. 9827--9838.  Matthew O'Kelly Aman Sinha Hongseok Namkoong Russ Tedrake and John C Duchi. 2018. Scalable end-to-end autonomous vehicle testing via rare-event simulation. In Advances in Neural Information Processing Systems. 9827--9838."},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/IV47402.2020.9304821"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/IVS.2017.7995918"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2012.6227127"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40648-0_14"},{"key":"e_1_2_1_52_1","unstructured":"Guodong Rong Byung Hyun Shin Hadi Tabatabaee Qiang Lu Steve Lemke Martins Mozeiko Eric Boise Geehoon Uhm Mark Gerow Shalin Mehta et al.[n.d.]. LGSVL Simulator: A High Fidelity Simulator for Autonomous Driving.([n. d.]).  Guodong Rong Byung Hyun Shin Hadi Tabatabaee Qiang Lu Steve Lemke Martins Mozeiko Eric Boise Geehoon Uhm Mark Gerow Shalin Mehta et al.[n.d.]. LGSVL Simulator: A High Fidelity Simulator for Autonomous Driving.([n. d.])."},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3154502"},{"key":"e_1_2_1_54_1","unstructured":"Shai Shalev-Shwartz Shaked Shammah and Amnon Shashua. 2017. On a Formal Model of Safe and Scalable Self-driving Cars. CoRR(2017).  Shai Shalev-Shwartz Shaked Shammah and Amnon Shashua. 2017. On a Formal Model of Safe and Scalable Self-driving Cars. CoRR(2017)."},{"key":"e_1_2_1_55_1","volume-title":"12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16)","author":"Sigurbjarnarson Helgi","year":"2016","unstructured":"Helgi Sigurbjarnarson , James Bornholt , Emina Torlak , and Xi Wang . 2016 . Push-Button Verification of File Systems via Crash Refinement . In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16) . Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, and Xi Wang. 2016. Push-Button Verification of File Systems via Crash Refinement. In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16)."},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2892208.2892235"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180220"},{"key":"e_1_2_1_58_1","doi-asserted-by":"crossref","unstructured":"Chris Urmson Joshua Anhalt Drew Bagnell Christopher Baker Robert Bittner M. N. Clark John Dolan Dave Duggins Tugrul Galatali Chris Geyer Michele Gittleman Sam Harbaugh Martial Hebert Thomas M. Howard Sascha Kolski Alonzo Kelly Maxim Likhachev Matt McNaughton Nick Miller Kevin Peterson Brian Pilnick Raj Rajkumar Paul Rybski Bryan Salesky Young-Woo Seo Sanjiv Singh Jarrod Snider Anthony Stentz William \"Red\" Whittaker Ziv Wolkowicki Jason Ziglar Hong Bae Thomas Brown Daniel Demitrish Bakhtiar Litkouhi Jim Nickolaou Varsha Sadekar Wende Zhang Joshua Struble Michael Taylor Michael Darms and Dave Ferguson. 2008. Autonomous Driving in Urban Environments: Boss and the Urban Challenge. Journal of Field Robotics(2008).  Chris Urmson Joshua Anhalt Drew Bagnell Christopher Baker Robert Bittner M. N. Clark John Dolan Dave Duggins Tugrul Galatali Chris Geyer Michele Gittleman Sam Harbaugh Martial Hebert Thomas M. Howard Sascha Kolski Alonzo Kelly Maxim Likhachev Matt McNaughton Nick Miller Kevin Peterson Brian Pilnick Raj Rajkumar Paul Rybski Bryan Salesky Young-Woo Seo Sanjiv Singh Jarrod Snider Anthony Stentz William \"Red\" Whittaker Ziv Wolkowicki Jason Ziglar Hong Bae Thomas Brown Daniel Demitrish Bakhtiar Litkouhi Jim Nickolaou Varsha Sadekar Wende Zhang Joshua Struble Michael Taylor Michael Darms and Dave Ferguson. 2008. Autonomous Driving in Urban Environments: Boss and the Urban Challenge. Journal of Field Robotics(2008).","DOI":"10.1002\/rob.20255"},{"key":"e_1_2_1_59_1","volume-title":"Proceedings of the ACM on Programming Languages 2, POPL","author":"Vazou Niki","year":"2017","unstructured":"Niki Vazou , Anish Tondwalkar , Vikraman Choudhury , Ryan G Scott , Ryan R Newton , Philip Wadler , and Ranjit Jhala .2017. Refinement reflection: complete verification with SMT . Proceedings of the ACM on Programming Languages 2, POPL ( 2017 ), 1--31. Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G Scott, Ryan R Newton, Philip Wadler, and Ranjit Jhala.2017. Refinement reflection: complete verification with SMT. Proceedings of the ACM on Programming Languages 2, POPL (2017), 1--31."},{"key":"e_1_2_1_60_1","volume-title":"2014 IEEE Intelligent Vehicles Symposium Proceedings.","author":"Wei J.","unstructured":"J. Wei , J. M. Snider , T. Gu , J. M. Dolan , and B. Litkouhi . 2014. A behavioral planning framework for autonomous driving . In 2014 IEEE Intelligent Vehicles Symposium Proceedings. J. Wei, J. M. Snider, T. Gu, J. M. Dolan, and B. Litkouhi. 2014. A behavioral planning framework for autonomous driving. In 2014 IEEE Intelligent Vehicles Symposium Proceedings."},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3238187"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1109\/IVS.2016.7535378"}],"container-title":["Proceedings of the ACM on Measurement and Analysis of Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3460082","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3460082","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3460082","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:28:28Z","timestamp":1750195708000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3460082"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6]]},"references-count":61,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2021,6]]}},"alternative-id":["10.1145\/3460082"],"URL":"https:\/\/doi.org\/10.1145\/3460082","relation":{},"ISSN":["2476-1249"],"issn-type":[{"value":"2476-1249","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,6]]},"assertion":[{"value":"2021-06-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}