{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T20:41:43Z","timestamp":1775680903048,"version":"3.50.1"},"reference-count":73,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T00:00:00Z","timestamp":1570665600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["1712067"],"award-info":[{"award-number":["1712067"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"DARPA","doi-asserted-by":"crossref","award":["8750-15-2-0096"],"award-info":[{"award-number":["8750-15-2-0096"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,10,10]]},"abstract":"<jats:p>Relational verification aims to prove properties that relate a pair of programs or two different runs of the same program. While relational properties (e.g., equivalence, non-interference) can be verified by reducing them to standard safety, there are typically many possible reduction strategies, only some of which result in successful automated verification. Motivated by this problem, we propose a novel relational verification algorithm that learns useful reduction strategies using reinforcement learning. Specifically, we show how to formulate relational verification as a Markov Decision Process (MDP) and use reinforcement learning to synthesize an optimal policy for the underlying MDP. The learned policy is then used to guide the search for a successful verification strategy. We have implemented this approach in a tool called Coeus and evaluate it on two benchmark suites. Our evaluation shows that Coeus solves significantly more problems within a given time limit compared to multiple baselines, including two state-of-the-art relational verification tools.<\/jats:p>","DOI":"10.1145\/3360567","type":"journal-article","created":{"date-parts":[[2019,10,11]],"date-time":"2019-10-11T14:53:33Z","timestamp":1570805613000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Relational verification using reinforcement learning"],"prefix":"10.1145","volume":"3","author":[{"given":"Jia","family":"Chen","sequence":"first","affiliation":[{"name":"University of Texas at Austin, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jiayi","family":"Wei","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yu","family":"Feng","sequence":"additional","affiliation":[{"name":"University of California at Santa Barbara, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Osbert","family":"Bastani","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Isil","family":"Dillig","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,10,10]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"Deepcoder: Learning to write programs. In ICLR.","author":"Balog Matej","year":"2016"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21437-0_17"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2016.05.004"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2004.1310735"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103670"},{"key":"e_1_2_2_6_1","unstructured":"Osbert Bastani Yewen Pu and Armando Solar-Lezama. 2018a. Verifiable reinforcement learning via policy extraction. In NIPS.  Osbert Bastani Yewen Pu and Armando Solar-Lezama. 2018a. Verifiable reinforcement learning via policy extraction. In NIPS."},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062349"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192383"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993524"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964003"},{"key":"e_1_2_2_11_1","volume-title":"International Conference on Machine Learning. 2933\u20132942","author":"Bielik Pavol","year":"2016"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_12"},{"key":"e_1_2_2_13_1","doi-asserted-by":"crossref","volume-title":"Horn clause solvers for program verification","author":"Bj\u00f8rner Nikolaj","DOI":"10.1007\/978-3-319-23534-9_2"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134058"},{"key":"e_1_2_2_15_1","volume-title":"AAAI","volume":"1992","author":"Chrisman Lonnie","year":"1992"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950342"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/1891823.1891830"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53413-7_8"},{"key":"e_1_2_2_20_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"de Moura Leonardo"},{"key":"e_1_2_2_21_1","volume-title":"Modular Product Programs. In European Symposium on Programming. Springer, 502\u2013529","author":"Eilers Marco","year":"2018"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2642937.2642987"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192382"},{"key":"e_1_2_2_24_1","volume-title":"Isil Dillig, and Swarat Chaudhuri.","author":"Feng Yu","year":"2017"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/647540.730008"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/3155562.3155573"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.1982.10014"},{"key":"e_1_2_2_28_1","unstructured":"Xiaoxiao Guo Satinder Singh Honglak Lee Richard L Lewis and Xiaoshi Wang. 2014. Deep learning for real-time Atari game play using offline Monte-Carlo tree search planning. In Advances in neural information processing systems. 3338\u20133346.  Xiaoxiao Guo Satinder Singh Honglak Lee Richard L Lewis and Xiaoshi Wang. 2014. Deep learning for real-time Atari game play using offline Monte-Carlo tree search planning. In Advances in neural information processing systems. 3338\u20133346."},{"key":"e_1_2_2_29_1","volume-title":"Navas","author":"Gurfinkel Arie","year":"2015"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908121"},{"key":"e_1_2_2_31_1","unstructured":"Geoffrey Irving Christian Szegedy Alexander A Alemi Niklas E\u00e9n Fran\u00e7ois Chollet and Josef Urban. 2016. Deepmath-deep sequence models for premise selection. In Advances in Neural Information Processing Systems. 2235\u20132243.  Geoffrey Irving Christian Szegedy Alexander A Alemi Niklas E\u00e9n Fran\u00e7ois Chollet and Josef Urban. 2016. Deepmath-deep sequence models for premise selection. In Advances in Neural Information Processing Systems. 2235\u20132243."},{"key":"e_1_2_2_32_1","unstructured":"Ashwin Kalyan Abhishek Mohta Oleksandr Polozov Dhruv Batra Prateek Jain and Sumit Gulwani. 2018. Neural-Guided Deductive Search for Real-Time Program Synthesis from Examples. In ICLR.  Ashwin Kalyan Abhishek Mohta Oleksandr Polozov Dhruv Batra Prateek Jain and Sumit Gulwani. 2018. Neural-Guided Deductive Search for Real-Time Program Synthesis from Examples. In ICLR."},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0249-4"},{"key":"e_1_2_2_34_1","volume-title":"Proceedings of the 7th symposium on Operating systems design and implementation. 161\u2013176","author":"Kremenek Ted","year":"2006"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_54"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491452"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192410"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926391"},{"key":"e_1_2_2_40_1","volume-title":"Scalable statistical bug isolation. 40, 6","author":"Liblit Ben","year":"2005"},{"key":"e_1_2_2_41_1","volume-title":"Merlin: specification inference for explicit information flow problems","author":"Livshits Benjamin"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786851"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/B978-1-55860-307-3.50031-9"},{"key":"e_1_2_2_44_1","unstructured":"William H Montgomery and Sergey Levine. 2016. Guided policy search via approximate mirror descent. In Advances in Neural Information Processing Systems. 4008\u20134016.  William H Montgomery and Sergey Levine. 2016. Guided policy search via approximate mirror descent. In Advances in Neural Information Processing Systems. 4008\u20134016."},{"key":"e_1_2_2_45_1","volume-title":"EPiC Series in Computing. EasyChair","author":"Mordvinov Dmitry","year":"2017"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908099"},{"key":"e_1_2_2_47_1","unstructured":"Adam Paszke Sam Gross Soumith Chintala Gregory Chanan Edward Yang Zachary DeVito Zeming Lin Alban Desmaison Luca Antiga and Adam Lerer. 2017. Automatic differentiation in PyTorch. In NIPS-W.  Adam Paszke Sam Gross Soumith Chintala Gregory Chanan Edward Yang Zachary DeVito Zeming Lin Alban Desmaison Luca Antiga and Adam Lerer. 2017. Automatic differentiation in PyTorch. In NIPS-W."},{"key":"e_1_2_2_48_1","volume-title":"Translation Validation. In Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS \u201998)","author":"Pnueli Amir","year":"1998"},{"key":"e_1_2_2_49_1","volume-title":"The ROSE Source-to-Source Compiler Infrastructure. In Cetus Users and Compiler Infrastructure Workshop, in conjunction with PACT","author":"Quinlan Dan","year":"2011"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192417"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984041"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837671"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677009"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2666356.2594321"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2451116.2451150"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2666356.2594302"},{"key":"e_1_2_2_57_1","volume-title":"International Conference on Machine Learning. 1889\u20131897","author":"Schulman John","year":"2015"},{"key":"e_1_2_2_58_1","doi-asserted-by":"crossref","unstructured":"Rahul Sharma and Alex Aiken. 2014. From invariant checking to invariant inference using randomized search. In CAV.  Rahul Sharma and Alex Aiken. 2014. From invariant checking to invariant inference using randomized search. In CAV.","DOI":"10.1007\/978-3-319-08867-9_6"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38856-9_21"},{"key":"e_1_2_2_60_1","unstructured":"Xujie Si Hanjun Dai Mukund Raghothaman Mayur Naik and Le Song. 2018a. Learning loop invariants for program verification. In Advances in Neural Information Processing Systems. 7762\u20137773.  Xujie Si Hanjun Dai Mukund Raghothaman Mayur Naik and Le Song. 2018a. Learning loop invariants for program verification. In Advances in Neural Information Processing Systems. 7762\u20137773."},{"key":"e_1_2_2_61_1","unstructured":"Xujie Si Yuan Yang Hanjun Dai Mayur Naik and Le Song. 2018b. Learning a Meta-Solver for Syntax-Guided Program Synthesis. In ICLR.  Xujie Si Yuan Yang Hanjun Dai Mayur Naik and Le Song. 2018b. Learning a Meta-Solver for Syntax-Guided Program Synthesis. In ICLR."},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1038\/nature16961"},{"key":"e_1_2_2_63_1","doi-asserted-by":"crossref","unstructured":"David Silver Julian Schrittwieser Karen Simonyan Ioannis Antonoglou Aja Huang Arthur Guez Thomas Hubert Lucas Baker Matthew Lai Adrian Bolton etal 2017. Mastering the game of go without human knowledge. Nature 550 7676 (2017) 354.  David Silver Julian Schrittwieser Karen Simonyan Ioannis Antonoglou Aja Huang Arthur Guez Thomas Hubert Lucas Baker Matthew Lai Adrian Bolton et al. 2017. Mastering the game of go without human knowledge. Nature 550 7676 (2017) 354.","DOI":"10.1038\/nature24270"},{"key":"e_1_2_2_64_1","volume-title":"Fast Numerical Program Analysis with Reinforcement Learning. In International Conference on Computer Aided Verification. Springer, 211\u2013229","author":"Singh Gagandeep","year":"2018"},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908092"},{"key":"e_1_2_2_66_1","volume-title":"Verifying Semantic Conflict-Freedom in Three-Way Program Merges. arXiv preprint arXiv:1802.06551","author":"Sousa Marcelo","year":"2018"},{"key":"e_1_2_2_67_1","volume-title":"Reinforcement learning: An introduction","author":"Sutton Richard S"},{"key":"e_1_2_2_68_1","unstructured":"Richard S Sutton David A McAllester Satinder P Singh and Yishay Mansour. 2000. Policy gradient methods for reinforcement learning with function approximation. In Advances in neural information processing systems. 1057\u20131063.  Richard S Sutton David A McAllester Satinder P Singh and Yishay Mansour. 2000. Policy gradient methods for reinforcement learning with function approximation. In Advances in neural information processing systems. 1057\u20131063."},{"key":"e_1_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_24"},{"key":"e_1_2_2_70_1","volume-title":"Shavlik","author":"Towell Geoffrey","year":"1992"},{"key":"e_1_2_2_71_1","unstructured":"Mingzhe Wang Yihe Tang Jian Wang and Jia Deng. 2017. Premise selection for theorem proving by deep graph embedding. In Advances in Neural Information Processing Systems. 2786\u20132796.  Mingzhe Wang Yihe Tang Jian Wang and Jia Deng. 2017. Premise selection for theorem proving by deep graph embedding. In Advances in Neural Information Processing Systems. 2786\u20132796."},{"key":"e_1_2_2_72_1","volume-title":"Deeppath: A reinforcement learning method for knowledge graph reasoning. In EMNLP.","author":"Xiong Wenhan","year":"2017"},{"key":"e_1_2_2_73_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.036"},{"key":"e_1_2_2_74_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_5"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360567","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360567","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360567","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:22:59Z","timestamp":1750202579000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360567"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,10]]},"references-count":73,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2019,10,10]]}},"alternative-id":["10.1145\/3360567"],"URL":"https:\/\/doi.org\/10.1145\/3360567","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,10,10]]},"assertion":[{"value":"2019-10-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}