{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,17]],"date-time":"2026-03-17T06:04:31Z","timestamp":1773727471979,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":40,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,6,8]],"date-time":"2019-06-08T00:00:00Z","timestamp":1559952000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,6,8]]},"DOI":"10.1145\/3314221.3314596","type":"proceedings-article","created":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T21:02:18Z","timestamp":1559941338000},"page":"1027-1040","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":74,"title":["Semantic program alignment for equivalence checking"],"prefix":"10.1145","author":[{"given":"Berkeley","family":"Churchill","sequence":"first","affiliation":[{"name":"Stanford University, USA"}]},{"given":"Oded","family":"Padon","sequence":"additional","affiliation":[{"name":"Stanford University, USA"}]},{"given":"Rahul","family":"Sharma","sequence":"additional","affiliation":[{"name":"Microsoft Research, India"}]},{"given":"Alex","family":"Aiken","sequence":"additional","affiliation":[{"name":"Stanford University, USA"}]}],"member":"320","published-online":{"date-parts":[[2019,6,8]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837656"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"crossref","unstructured":"Clark Barrett Christopher L. Conway Morgan Deters Liana Hadarean Dejan Jovanovi\u2019c Tim King Andrew Reynolds and Cesare Tinelli. 2011. CVC4. In Computer Aided Verification (CAV \u201911). 171\u2013177.   Clark Barrett Christopher L. Conway Morgan Deters Liana Hadarean Dejan Jovanovi\u2019c Tim King Andrew Reynolds and Cesare Tinelli. 2011. CVC4. In Computer Aided Verification (CAV \u201911). 171\u2013177.","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2442516.2442529"},{"key":"e_1_3_2_2_4_1","volume-title":"Relational Verification Using Product Programs. In International Conference on Formal Methods (FM \u201911)","author":"Barthe Gilles","year":"2011","unstructured":"Gilles Barthe , Juan Manuel Crespo , and C\u00e9sar Kunz . 2011 . Relational Verification Using Product Programs. In International Conference on Formal Methods (FM \u201911) . 200\u2013214. Gilles Barthe, Juan Manuel Crespo, and C\u00e9sar Kunz. 2011. Relational Verification Using Product Programs. In International Conference on Formal Methods (FM \u201911). 200\u2013214."},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964003"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3037697.3037754"},{"key":"e_1_3_2_2_7_1","volume-title":"Black-Box Equivalence Checking Across Compiler Optimizations. In Asian Symposium on Programing Languages and Systems (APLAS \u201917)","author":"Dahiya Manjeet","year":"2017","unstructured":"Manjeet Dahiya and Sorav Bansal . 2017 . Black-Box Equivalence Checking Across Compiler Optimizations. In Asian Symposium on Programing Languages and Systems (APLAS \u201917) . 127\u2013147. Manjeet Dahiya and Sorav Bansal. 2017. Black-Box Equivalence Checking Across Compiler Optimizations. In Asian Symposium on Programing Languages and Systems (APLAS \u201917). 127\u2013147."},{"key":"e_1_3_2_2_8_1","volume-title":"Modeling Undefined Behavior Semantics for Checking Equivalence Across Compiler Optimizations. In Haifa Verification Conference (HVC \u201917)","author":"Dahiya Manjeet","year":"2017","unstructured":"Manjeet Dahiya and Sorav Bansal . 2017 . Modeling Undefined Behavior Semantics for Checking Equivalence Across Compiler Optimizations. In Haifa Verification Conference (HVC \u201917) . Manjeet Dahiya and Sorav Bansal. 2017. Modeling Undefined Behavior Semantics for Checking Equivalence Across Compiler Optimizations. In Haifa Verification Conference (HVC \u201917)."},{"key":"e_1_3_2_2_9_1","volume-title":"Relational Verification Through Horn Clause Transformation. In International Static Analysis Symposium (SAS \u201916)","author":"Angelis Emanuele De","year":"2016","unstructured":"Emanuele De Angelis , Fabio Fioravanti , Alberto Pettorossi , and Maurizio Proietti . 2016 . Relational Verification Through Horn Clause Transformation. In International Static Analysis Symposium (SAS \u201916) . 147\u2013169. Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, and Maurizio Proietti. 2016. Relational Verification Through Horn Clause Transformation. In International Static Analysis Symposium (SAS \u201916). 147\u2013169."},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"crossref","unstructured":"Emanuele De Angelis Fabio Fioravanti Alberto Pettorossi and Maurizio Proietti. 2017. Enhancing Predicate Pairing with Abstraction for Relational Verification. In Logic-Based Program Synthesis and Transformation (LOPSTR \u201917).  Emanuele De Angelis Fabio Fioravanti Alberto Pettorossi and Maurizio Proietti. 2017. Enhancing Predicate Pairing with Abstraction for Relational Verification. In Logic-Based Program Synthesis and Transformation (LOPSTR \u201917).","DOI":"10.1007\/978-3-319-94460-9_17"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"crossref","unstructured":"Leonardo De Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS \u201908). 337\u2013340.   Leonardo De Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS \u201908). 337\u2013340.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.5220\/0005869501950202"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48899-7_42"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2642937.2642987"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/647540.730008"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"crossref","unstructured":"Shubhani Gupta Aseem Saxena Anmol Mahajan and Sorav Bansal. 2018. Effective Use of SMT Solvers for Program Equivalence Checking Through Invariant-Sketching and Query-Decomposition. In Theory and Applications of Satisfiability Testing (SAT \u201918).  Shubhani Gupta Aseem Saxena Anmol Mahajan and Sorav Bansal. 2018. Effective Use of SMT Solvers for Program Equivalence Checking Through Invariant-Sketching and Query-Decomposition. In Theory and Applications of Satisfiability Testing (SAT \u201918).","DOI":"10.1007\/978-3-319-94144-8_22"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491442"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908121"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_2_20_1","volume-title":"Relational Program Reasoning Using Compiler IR. In Working Conference on Verified Software: Theories, Tools, and Experiments. 149\u2013165","author":"Kiefer Moritz","year":"2016","unstructured":"Moritz Kiefer , Vladimir Klebanov , and Mattias Ulbrich . 2016 . Relational Program Reasoning Using Compiler IR. In Working Conference on Verified Software: Theories, Tools, and Experiments. 149\u2013165 . Moritz Kiefer, Vladimir Klebanov, and Mattias Ulbrich. 2016. Relational Program Reasoning Using Compiler IR. In Working Conference on Verified Software: Theories, Tools, and Experiments. 149\u2013165."},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542513"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737965"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0366-1"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/PACT.2011.68"},{"key":"e_1_3_2_2_25_1","unstructured":"Dmitry Mordvinov and Grigory Fedyukovich. 2017. Synchronizing Constrained Horn Clauses. In LPAR. 338\u2013355.  Dmitry Mordvinov and Grigory Fedyukovich. 2017. Synchronizing Constrained Horn Clauses. In LPAR. 338\u2013355."},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349314"},{"key":"e_1_3_2_2_27_1","volume-title":"Abstract Semantic Differencing for Numerical Programs. In Static Analysis Symposium (SAS \u201913)","author":"Partush Nimrod","year":"2013","unstructured":"Nimrod Partush and Eran Yahav . 2013 . Abstract Semantic Differencing for Numerical Programs. In Static Analysis Symposium (SAS \u201913) . 238\u2013 258. Nimrod Partush and Eran Yahav. 2013. Abstract Semantic Differencing for Numerical Programs. In Static Analysis Symposium (SAS \u201913). 238\u2013 258."},{"key":"e_1_3_2_2_28_1","volume-title":"Engler","author":"Ramos David A.","year":"2011","unstructured":"David A. Ramos and Dawson R . Engler . 2011 . Practical, Low- Effort Equivalence Verification of Real Code. In Computer Aided Verification (CAV \u201911). 669\u2013685. David A. Ramos and Dawson R. Engler. 2011. Practical, Low-Effort Equivalence Verification of Real Code. In Computer Aided Verification (CAV \u201911). 669\u2013685."},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2490301.2451150"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"crossref","unstructured":"Markus Schordan Pei-Hung Lin Dan Quinlan and Louis-No\u00ebl Pouchet. 2014. Verification of Polyhedral Optimizations with Constant Loop Bounds in Finite State Space Computations. In Leveraging Applications of Formal Methods Verification and Validation. Specialized Techniques and Applications. 493\u2013508.  Markus Schordan Pei-Hung Lin Dan Quinlan and Louis-No\u00ebl Pouchet. 2014. Verification of Polyhedral Optimizations with Constant Loop Bounds in Finite State Space Computations. In Leveraging Applications of Formal Methods Verification and Validation. Specialized Techniques and Applications. 493\u2013508.","DOI":"10.1007\/978-3-662-45231-8_41"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"crossref","unstructured":"Thomas Arthur Leck Sewell Magnus O. Myreen and Gerwin Klein. 2013. Translation Validation for a Verified OS Kernel. In Programming Language Design and Implementation (PLDI \u201913). 471\u2013482.  Thomas Arthur Leck Sewell Magnus O. Myreen and Gerwin Klein. 2013. Translation Validation for a Verified OS Kernel. In Programming Language Design and Implementation (PLDI \u201913). 471\u2013482.","DOI":"10.1145\/2499370.2462183"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509509"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814278"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"crossref","unstructured":"Michael Stepp Ross Tate and Sorin Lerner. 2011. Equality-Based Translation Validator for LLVM. In Computer Aided Verification (CAV \u201911). 737\u2013742.   Michael Stepp Ross Tate and Sorin Lerner. 2011. Equality-Based Translation Validator for LLVM. In Computer Aided Verification (CAV \u201911). 737\u2013742.","DOI":"10.1007\/978-3-642-22110-1_59"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480915"},{"key":"e_1_3_2_2_36_1","unstructured":"The Sage Developers. 2017. SageMath the Sage Mathematics Software System (Version 7.5.1). http:\/\/www.sagemath.org.  The Sage Developers. 2017. SageMath the Sage Mathematics Software System (Version 7.5.1). http:\/\/www.sagemath.org."},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993533"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2362389.2362390"},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"crossref","unstructured":"Wei Wang Clark Barrett and Thomas Wies. 2017. Partitioned Memory Models for Program Analysis. In Verification Model Checking and Abstract Interpretation (VMCAI \u201917). 539\u2013558.  Wei Wang Clark Barrett and Thomas Wies. 2017. Partitioned Memory Models for Program Analysis. In Verification Model Checking and Abstract Interpretation (VMCAI \u201917). 539\u2013558.","DOI":"10.1007\/978-3-319-52234-0_29"},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_5"}],"event":{"name":"PLDI '19: 40th ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Phoenix AZ USA","acronym":"PLDI '19","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3314596","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3314221.3314596","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:53:22Z","timestamp":1750204402000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3314596"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,6,8]]},"references-count":40,"alternative-id":["10.1145\/3314221.3314596","10.1145\/3314221"],"URL":"https:\/\/doi.org\/10.1145\/3314221.3314596","relation":{},"subject":[],"published":{"date-parts":[[2019,6,8]]},"assertion":[{"value":"2019-06-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}