{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,24]],"date-time":"2024-07-24T23:11:22Z","timestamp":1721862682531},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T00:00:00Z","timestamp":1641945600000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CCF-1160904, CCF-1409813"],"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 Program. Lang."],"published-print":{"date-parts":[[2022,1,16]]},"abstract":"\n Many invariant inference techniques reason simultaneously about states and predicates, and it is well-known that these two kinds of reasoning are in some sense dual to each other. We present a new formal duality between states and predicates, and use it to derive a new primal-dual invariant inference algorithm. The new\n induction duality<\/jats:italic>\n is based on a notion of provability by incremental induction that is formally dual to reachability, and the duality is surprisingly symmetric. The symmetry allows us to derive the dual of the well-known Houdini algorithm, and by combining Houdini with its dual image we obtain\n primal-dual Houdini<\/jats:italic>\n , the first truly primal-dual invariant inference algorithm. An early prototype of primal-dual Houdini for the domain of distributed protocol verification can handle difficult benchmarks from the literature.\n <\/jats:p>","DOI":"10.1145\/3498712","type":"journal-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T17:03:12Z","timestamp":1642006992000},"page":"1-29","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Induction duality: primal-dual search for invariants"],"prefix":"10.1145","volume":"6","author":[{"given":"Oded","family":"Padon","sequence":"first","affiliation":[{"name":"VMware Research, USA \/ Stanford University, USA"}]},{"given":"James R.","family":"Wilcox","sequence":"additional","affiliation":[{"name":"Certora, USA"}]},{"given":"Jason R.","family":"Koenig","sequence":"additional","affiliation":[{"name":"Stanford University, USA"}]},{"given":"Kenneth L.","family":"McMillan","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, USA"}]},{"given":"Alex","family":"Aiken","sequence":"additional","affiliation":[{"name":"Stanford University, USA"}]}],"member":"320","published-online":{"date-parts":[[2022,1,12]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31612-8_1"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-008-0080-9"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_23"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(00)00196-4"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45251-6_29"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_5"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706307"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-76384-8_9"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.34727\/2021\/isbn.978-3-85448-046-4_20"},{"key":"e_1_2_2_18_1","volume-title":"Small (Enough) World After All. In 18th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2021","author":"Hance Travis","year":"2021","unstructured":"Travis Hance , Marijn Heule , Ruben Martins , and Bryan Parno . 2021 . Finding Invariants of Distributed Systems: It\u2019 s a Small (Enough) World After All. In 18th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2021 , April 12-14, 2021, James Mickens and Renata Teixeira (Eds.). USENIX Association, 115\u2013131. https:\/\/www.usenix.org\/conference\/nsdi21\/presentation\/hance Travis Hance, Marijn Heule, Ruben Martins, and Bryan Parno. 2021. Finding Invariants of Distributed Systems: It\u2019 s a Small (Enough) World After All. In 18th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2021, April 12-14, 2021, James Mickens and Renata Teixeira (Eds.). USENIX Association, 115\u2013131. https:\/\/www.usenix.org\/conference\/nsdi21\/presentation\/hance"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03237-0_7"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_18"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_33"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3022187"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386018"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/568425.568433"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1111\/j.1746-8361.1969.tb01194.x"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359651"},{"key":"e_1_2_2_28_1","unstructured":"Dahlia Malkhi Leslie Lamport and Lidong Zhou. 2008. Stoppable Paxos. https:\/\/www.microsoft.com\/en-us\/research\/publication\/stoppable-paxos\/ Dahlia Malkhi Leslie Lamport and Lidong Zhou. 2008. Stoppable Paxos. https:\/\/www.microsoft.com\/en-us\/research\/publication\/stoppable-paxos\/"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_14"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_16"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385967"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-32304-2_16"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140568"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908118"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.5703081"},{"key":"e_1_2_2_38_1","volume-title":"The Galois connection of syntax and semantics","author":"Smith Peter","unstructured":"Peter Smith . 2010. The Galois connection of syntax and semantics . Cambridge University . http:\/\/www.logicmatters.net\/resources\/pdfs\/Galois.pdf Peter Smith. 2010. The Galois connection of syntax and semantics. Cambridge University. http:\/\/www.logicmatters.net\/resources\/pdfs\/Galois.pdf"},{"key":"e_1_2_2_39_1","volume-title":"International Conference on Formal Methods in Computer-Aided Design, FMCAD \u201911","author":"Somenzi Fabio","year":"2011","unstructured":"Fabio Somenzi and Aaron R. Bradley . 2011. IC3: where monolithic and incremental meet . In International Conference on Formal Methods in Computer-Aided Design, FMCAD \u201911 , Austin, TX, USA, October 30 - November 02, 2011 , Per Bjesse and Anna Slobodov\u00e1 (Eds.). FMCAD Inc., 3\u20138. http:\/\/dl.acm.org\/citation.cfm?id=2157657 Fabio Somenzi and Aaron R. Bradley. 2011. IC3: where monolithic and incremental meet. In International Conference on Formal Methods in Computer-Aided Design, FMCAD \u201911, Austin, TX, USA, October 30 - November 02, 2011, Per Bjesse and Anna Slobodov\u00e1 (Eds.). FMCAD Inc., 3\u20138. http:\/\/dl.acm.org\/citation.cfm?id=2157657"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192414"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_2_2_42_1","volume-title":"DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols. In 15th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2021","author":"Yao Jianan","year":"2021","unstructured":"Jianan Yao , Runzhou Tao , Ronghui Gu , Jason Nieh , Suman Jana , and Gabriel Ryan . 2021 . DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols. In 15th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2021 , July 14-16, 2021, Angela Demke Brown and Jay R. Lorch (Eds.). USENIX Association, 405\u2013421. https:\/\/www.usenix.org\/conference\/osdi21\/presentation\/yao Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh, Suman Jana, and Gabriel Ryan. 2021. DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols. In 15th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2021, July 14-16, 2021, Angela Demke Brown and Jay R. Lorch (Eds.). USENIX Association, 405\u2013421. https:\/\/www.usenix.org\/conference\/osdi21\/presentation\/yao"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498712","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498712","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,2]],"date-time":"2023-01-02T00:12:43Z","timestamp":1672618363000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498712"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,12]]},"references-count":42,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2022,1,16]]}},"alternative-id":["10.1145\/3498712"],"URL":"https:\/\/doi.org\/10.1145\/3498712","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,1,12]]},"assertion":[{"value":"2022-01-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}