{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T04:34:09Z","timestamp":1781238849891,"version":"3.54.1"},"reference-count":46,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T00:00:00Z","timestamp":1697414400000},"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":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,10,16]]},"abstract":"<jats:p>We introduce a novel notion of perception contracts to reason about the safety of controllers that interact with an environment using neural perception. Perception contracts capture errors in ground-truth estimations that preserve invariants when systems act upon them. We develop a theory of perception contracts and design symbolic learning algorithms for synthesizing them from a finite set of images. We implement our algorithms and evaluate synthesized perception contracts for two realistic vision-based control systems, a lane tracking system for an electric vehicle and an agricultural robot that follows crop rows. Our evaluation shows that our approach is effective in synthesizing perception contracts and generalizes well when evaluated over test images obtained during runtime monitoring of the systems.<\/jats:p>","DOI":"10.1145\/3622875","type":"journal-article","created":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T15:41:29Z","timestamp":1697470889000},"page":"2196-2223","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Perception Contracts for Safety of ML-Enabled Systems"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7996-4798","authenticated-orcid":false,"given":"Angello","family":"Astorga","sequence":"first","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Urbana, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8339-9915","authenticated-orcid":false,"given":"Chiao","family":"Hsieh","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Urbana, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9782-721X","authenticated-orcid":false,"given":"P.","family":"Madhusudan","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Urbana, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6672-8470","authenticated-orcid":false,"given":"Sayan","family":"Mitra","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Urbana, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,10,16]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/EMSOFT55006.2022.00016"},{"key":"e_1_2_1_2_1","volume-title":"Principles of Cyber-Physical Systems","author":"Alur Rajeev","unstructured":"Rajeev Alur . 2015. Principles of Cyber-Physical Systems . MIT Press , Cambridge, MA . isbn:978-0-262-02911-7 Rajeev Alur. 2015. Principles of Cyber-Physical Systems. MIT Press, Cambridge, MA. isbn:978-0-262-02911-7"},{"key":"e_1_2_1_3_1","unstructured":"Rajeev Alur Rastislav Bod\u00edk Eric Dallal Dana Fisman Pranav Garg Garvit Juniwal Hadas Kress-Gazit P. Madhusudan Milo M. K. Martin Mukund Raghothaman Shambwaditya Saha Sanjit A. Seshia Rishabh Singh Armando Solar-Lezama Emina Torlak and Abhishek Udupa. 2015. Syntax-guided synthesis. In Dependable Software Systems Engineering (NATO Science for Peace and Security Series D: Information and Communication Security Vol. 40). \t\t\t\t  Rajeev Alur Rastislav Bod\u00edk Eric Dallal Dana Fisman Pranav Garg Garvit Juniwal Hadas Kress-Gazit P. Madhusudan Milo M. K. Martin Mukund Raghothaman Shambwaditya Saha Sanjit A. Seshia Rishabh Singh Armando Solar-Lezama Emina Torlak and Abhishek Udupa. 2015. Syntax-guided synthesis. In Dependable Software Systems Engineering (NATO Science for Peace and Security Series D: Information and Communication Security Vol. 40)."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1047659.1040314"},{"key":"e_1_2_1_5_1","volume-title":"Larus","author":"Ammons Glenn","year":"2002","unstructured":"Glenn Ammons , Rastislav Bod\u00edk , and James R . Larus . 2002 . Mining Specifications. In POPL 2002. Glenn Ammons, Rastislav Bod\u00edk, and James R. Larus. 2002. Mining Specifications. In POPL 2002."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314641"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485481"},{"key":"e_1_2_1_8_1","volume-title":"Murray","author":"Astrom Karl Johan","year":"2008","unstructured":"Karl Johan Astrom and Richard M . Murray . 2008 . Feedback Systems : An Introduction for Scientists and Engineers. Princeton University Press , Princeton, NJ, USA. isbn:0691135762, 9780691135762 Karl Johan Astrom and Richard M. Murray. 2008. Feedback Systems: An Introduction for Scientists and Engineers. Princeton University Press, Princeton, NJ, USA. isbn:0691135762, 9780691135762"},{"key":"e_1_2_1_9_1","unstructured":"Stanley Bak Changliu Liu and Taylor Johnson. 2021. The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results. arxiv:2109.00498. arxiv:2109.00498 \t\t\t\t  Stanley Bak Changliu Liu and Taylor Johnson. 2021. The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results. arxiv:2109.00498. arxiv:2109.00498"},{"key":"e_1_2_1_10_1","volume-title":"Johnson","author":"Bak Stanley","year":"2021","unstructured":"Stanley Bak , Changliu Liu , and Taylor T . Johnson . 2021 . The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results. CoRR , abs\/2109.00498 (2021), arXiv:2109.00498. arxiv:2109.00498 Stanley Bak, Changliu Liu, and Taylor T. Johnson. 2021. The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results. CoRR, abs\/2109.00498 (2021), arXiv:2109.00498. arxiv:2109.00498"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454056"},{"key":"e_1_2_1_12_1","volume-title":"TACAS\u201908\/ETAPS\u201908","author":"Moura Leonardo De","unstructured":"Leonardo De Moura and Nikolaj Bj\u00f8rner . 2008. Z3: An Efficient SMT Solver . In TACAS\u201908\/ETAPS\u201908 . Springer-Verlag , Berlin, Heidelberg . 337\u2013340. isbn:3540787992 Leonardo De Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In TACAS\u201908\/ETAPS\u201908. Springer-Verlag, Berlin, Heidelberg. 337\u2013340. isbn:3540787992"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_25"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/ITSC45102.2020.9294366"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/302405.302467"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53288-8_6"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10994-021-06120-5"},{"key":"e_1_2_1_18_1","volume-title":"Computer Aided Verification","author":"Garg Pranav","unstructured":"Pranav Garg , Christof L\u00f6ding , P. Madhusudan , and Daniel Neider . 2014. ICE:\u00a0A\u00a0Robust\u00a0Framework\u00a0for\u00a0Learning\u00a0Invariants. In Computer Aided Verification , Armin Biere and Roderick Bloem (Eds.). Springer International Publishing , Cham . 69\u201387. isbn:978-3-319-08867-9 Pranav Garg, Christof L\u00f6ding, P. Madhusudan, and Daniel Neider. 2014. ICE:\u00a0A\u00a0Robust\u00a0Framework\u00a0for\u00a0Learning\u00a0Invariants. In Computer Aided Verification, Armin Biere and Roderick Bloem (Eds.). Springer International Publishing, Cham. 69\u201387. isbn:978-3-319-08867-9"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2018.00058"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.23919\/ACC50511.2021.9482896"},{"key":"e_1_2_1_21_1","unstructured":"John E Gibson Eccles S McVey and Clive Douglas Leedham. 1961. Stability of nonlinear control systems by the second method of Liapunov. \t\t\t\t  John E Gibson Eccles S McVey and Clive Douglas Leedham. 1961. Stability of nonlinear control systems by the second method of Liapunov."},{"key":"e_1_2_1_22_1","unstructured":"LLC Gurobi Optimization. 2020. Gurobi Optimizer Reference Manual. http:\/\/www.gurobi.com \t\t\t\t  LLC Gurobi Optimization. 2020. Gurobi Optimizer Reference Manual. http:\/\/www.gurobi.com"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1081706.1081713"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACC.2007.4282788"},{"key":"#cr-split#-e_1_2_1_25_1.1","unstructured":"Chiao Hsieh Yangge Li Yubin Koh and Sayan Mitra. 2022. Assuring safety of vision-based swarm formation control. https:\/\/doi.org\/10.48550\/ARXIV.2210.00982 10.48550\/ARXIV.2210.00982"},{"key":"#cr-split#-e_1_2_1_25_1.2","unstructured":"Chiao Hsieh Yangge Li Yubin Koh and Sayan Mitra. 2022. Assuring safety of vision-based swarm formation control. https:\/\/doi.org\/10.48550\/ARXIV.2210.00982"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2022.3197508"},{"key":"e_1_2_1_27_1","volume-title":"Proc. 22nd ACM Int. Conf. HSCC. 169\u2013178","author":"Ivanov Radoslav","year":"2019","unstructured":"Radoslav Ivanov , James Weimer , Rajeev Alur , George J. Pappas , and Insup Lee . 2019 . Verisig: Verifying Safety Properties of Hybrid Systems with Neural Network Controllers . In Proc. 22nd ACM Int. Conf. HSCC. 169\u2013178 . isbn:9781450362825 Radoslav Ivanov, James Weimer, Rajeev Alur, George J. Pappas, and Insup Lee. 2019. Verisig: Verifying Safety Properties of Hybrid Systems with Neural Network Controllers. In Proc. 22nd ACM Int. Conf. HSCC. 169\u2013178. isbn:9781450362825"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2931037.2931062"},{"key":"e_1_2_1_29_1","first-page":"63387","volume-title":"Proc. 29th Int. Conf. CAV. 97\u2013117","author":"Katz Guy","unstructured":"Guy Katz , Clark Barrett , David L. Dill , Kyle Julian , and Mykel J. Kochenderfer . 2017. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks . In Proc. 29th Int. Conf. CAV. 97\u2013117 . isbn:978-3-319- 63387 - 63389 Guy Katz, Clark Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer. 2017. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. In Proc. 29th Int. Conf. CAV. 97\u2013117. isbn:978-3-319-63387-9"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/DASC52595.2021.9594360"},{"key":"e_1_2_1_31_1","volume-title":"Proceedings of the 38th International Conference on Machine Learning, ICML 2021","volume":"6222","author":"Leino Klas","year":"2021","unstructured":"Klas Leino , Zifan Wang , and Matt Fredrikson . 2021 . Globally-Robust Neural Networks . In Proceedings of the 38th International Conference on Machine Learning, ICML 2021 , 18-24 July 2021, Virtual Event, Marina Meila and Tong Zhang (Eds.) (Proceedings of Machine Learning Research , Vol. 139). PMLR, 6212\u2013 6222 . http:\/\/proceedings.mlr.press\/v139\/leino21a.html Klas Leino, Zifan Wang, and Matt Fredrikson. 2021. Globally-Robust Neural Networks. In Proceedings of the 38th International Conference on Machine Learning, ICML 2021, 18-24 July 2021, Virtual Event, Marina Meila and Tong Zhang (Eds.) (Proceedings of Machine Learning Research, Vol. 139). PMLR, 6212\u20136222. http:\/\/proceedings.mlr.press\/v139\/leino21a.html"},{"key":"e_1_2_1_32_1","volume-title":"Henzinger","author":"Lukina Anna","year":"2021","unstructured":"Anna Lukina , Christian Schilling , and Thomas A . Henzinger . 2021 . Into the Unknown : Active Monitoring of\u00a0Neural Networks. In Runtime Verification, Lu Feng and Dana Fisman (Eds.). Springer International Publishing , Cham. 42\u201361. isbn:978-3-030-88494-9 Anna Lukina, Christian Schilling, and Thomas A. Henzinger. 2021. Into the Unknown: Active Monitoring of\u00a0Neural Networks. In Runtime Verification, Lu Feng and Dana Fisman (Eds.). Springer International Publishing, Cham. 42\u201361. isbn:978-3-030-88494-9"},{"key":"e_1_2_1_33_1","volume-title":"Runtime Verification","author":"Mamouras Konstantinos","unstructured":"Konstantinos Mamouras , Agnishom Chattopadhyay , and Zhifu Wang . 2021. A Compositional Framework for\u00a0Quantitative Online Monitoring over\u00a0Continuous-Time Signals . In Runtime Verification , Lu Feng and Dana Fisman (Eds.). Springer International Publishing , Cham . 142\u2013163. isbn:978-3-030-88494-9 Konstantinos Mamouras, Agnishom Chattopadhyay, and Zhifu Wang. 2021. A Compositional Framework for\u00a0Quantitative Online Monitoring over\u00a0Continuous-Time Signals. In Runtime Verification, Lu Feng and Dana Fisman (Eds.). Springer International Publishing, Cham. 142\u2013163. isbn:978-3-030-88494-9"},{"key":"e_1_2_1_34_1","unstructured":"Thomas M. Mitchell. 1997. Machine Learning (1 ed.). \t\t\t\t  Thomas M. Mitchell. 1997. Machine Learning (1 ed.)."},{"key":"e_1_2_1_35_1","volume-title":"Verifying Cyber-Physical Systems: A Path to Safe Autonomy","author":"Mitra Sayan","unstructured":"Sayan Mitra . 2021. Verifying Cyber-Physical Systems: A Path to Safe Autonomy . MIT Press . isbn:978-0-262-04480-6 Sayan Mitra. 2021. Verifying Cyber-Physical Systems: A Path to Safe Autonomy. MIT Press. isbn:978-0-262-04480-6"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/IVS.2018.8500547"},{"key":"e_1_2_1_37_1","volume-title":"Induction of Decision Trees. Mach. Learn., 1, 1","author":"Quinlan J. R.","year":"1986","unstructured":"J. R. Quinlan . 1986. Induction of Decision Trees. Mach. Learn., 1, 1 ( 1986 ). J. R. Quinlan. 1986. Induction of Decision Trees. Mach. Learn., 1, 1 (1986)."},{"key":"e_1_2_1_38_1","volume-title":"NNLander-VeriF: A Neural Network Formal Verification Framework for\u00a0Vision-Based Autonomous Aircraft Landing","author":"Cruz Ulices Santa","unstructured":"Ulices Santa Cruz and Yasser Shoukry . 2022. NNLander-VeriF: A Neural Network Formal Verification Framework for\u00a0Vision-Based Autonomous Aircraft Landing . In NASA Formal Methods, Jyotirmoy V. Deshmukh, Klaus Havelund, and Ivan Perez (Eds.). Springer International Publishing , Cham . 213\u2013230. isbn:978-3-031-06773-0 Ulices Santa Cruz and Yasser Shoukry. 2022. NNLander-VeriF: A Neural Network Formal Verification Framework for\u00a0Vision-Based Autonomous Aircraft Landing. In NASA Formal Methods, Jyotirmoy V. Deshmukh, Klaus Havelund, and Ivan Perez (Eds.). Springer International Publishing, Cham. 213\u2013230. isbn:978-3-031-06773-0"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290354"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.15607\/RSS.2021.XVII.019"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-77653-6_3"},{"key":"e_1_2_1_42_1","volume-title":"Evaluating Robustness of Neural Networks with Mixed Integer Programming. In 7th International Conference on Learning Representations, ICLR 2019","author":"Tjeng Vincent","year":"2019","unstructured":"Vincent Tjeng , Kai Yuanqing Xiao , and Russ Tedrake . 2019 . Evaluating Robustness of Neural Networks with Mixed Integer Programming. In 7th International Conference on Learning Representations, ICLR 2019 , New Orleans, LA, USA , May 6-9, 2019. OpenReview.net. https:\/\/openreview.net\/forum?id=HyGIdiRqtm Vincent Tjeng, Kai Yuanqing Xiao, and Russ Tedrake. 2019. Evaluating Robustness of Neural Networks with Mixed Integer Programming. In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net. https:\/\/openreview.net\/forum?id=HyGIdiRqtm"},{"key":"e_1_2_1_43_1","first-page":"53288","volume-title":"Proc. 32nd Int. Conf. CAV. 3\u201317","author":"Tran Hoang-Dung","unstructured":"Hoang-Dung Tran , Xiaodong Yang , Diego Manzanas Lopez , Patrick Musau , Luan Viet Nguyen , Weiming Xiang , Stanley Bak , and Taylor T. Johnson . 2020. NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems . In Proc. 32nd Int. Conf. CAV. 3\u201317 . isbn:978-3-030- 53288 - 53288 Hoang-Dung Tran, Xiaodong Yang, Diego Manzanas Lopez, Patrick Musau, Luan Viet Nguyen, Weiming Xiang, Stanley Bak, and Taylor T. Johnson. 2020. NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems. In Proc. 32nd Int. Conf. CAV. 3\u201317. isbn:978-3-030-53288-8"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/566172.566212"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1134285.1134427"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622875","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3622875","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:57:27Z","timestamp":1750298247000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622875"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,16]]},"references-count":46,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2023,10,16]]}},"alternative-id":["10.1145\/3622875"],"URL":"https:\/\/doi.org\/10.1145\/3622875","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,10,16]]},"assertion":[{"value":"2023-10-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}