{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:10:12Z","timestamp":1775873412718,"version":"3.50.1"},"reference-count":65,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2017,2,28]],"date-time":"2017-02-28T00:00:00Z","timestamp":1488240000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"ERC","award":["321174-VSSC"],"award-info":[{"award-number":["321174-VSSC"]}]},{"name":"BSF","award":["2012259"],"award-info":[{"award-number":["2012259"]}]},{"name":"Broadcom Foundation and Tel Aviv University Authentication Initiative"},{"name":"EU FP7 project ADVENT","award":["308830"],"award-info":[{"award-number":["308830"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2017,2,28]]},"abstract":"<jats:p>\n            We present\n            <jats:italic>Universal Property Directed Reachability<\/jats:italic>\n            (PDR\n            <jats:sup>\u2200<\/jats:sup>\n            ), a property-directed semi-algorithm for automatic inference of invariants in a universal fragment of first-order logic. PDR\n            <jats:sup>\u2200<\/jats:sup>\n            is an extension of Bradley\u2019s PDR\/IC3 algorithm for inference of propositional invariants. PDR\n            <jats:sup>\u2200<\/jats:sup>\n            terminates when it discovers a concrete counterexample, infers an inductive universal invariant strong enough to establish the desired safety property, or finds a\n            <jats:italic>proof that such an invariant does not exist<\/jats:italic>\n            . PDR\n            <jats:sup>\u2200<\/jats:sup>\n            is not guaranteed to terminate. However, we prove that under certain conditions, for example, when reasoning about programs manipulating singly linked lists, it does.\n          <\/jats:p>\n          <jats:p>\n            We implemented an analyzer based on PDR\n            <jats:sup>\u2200<\/jats:sup>\n            and applied it to a collection of list-manipulating programs. Our analyzer was able to automatically infer universal invariants strong enough to establish memory safety and certain functional correctness properties, show the absence of such invariants for certain natural programs and specifications, and detect bugs. All this without the need for user-supplied abstraction predicates.\n          <\/jats:p>","DOI":"10.1145\/3022187","type":"journal-article","created":{"date-parts":[[2017,3,30]],"date-time":"2017-03-30T20:23:34Z","timestamp":1490905414000},"page":"1-33","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":27,"title":["Property-Directed Inference of Universal Invariants or Proving Their Absence"],"prefix":"10.1145","volume":"64","author":[{"given":"Aleksandr","family":"Karbyshev","sequence":"first","affiliation":[{"name":"Aarhus University, Aarhus N, Denmark"}]},{"given":"Nikolaj","family":"Bj\u00f8rner","sequence":"additional","affiliation":[{"name":"Microsoft Research, One Microsoft Way, Washington"}]},{"given":"Shachar","family":"Itzhaky","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, MA"}]},{"given":"Noam","family":"Rinetzky","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Tel Aviv, Israel"}]},{"given":"Sharon","family":"Shoham","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Tel Aviv, Israel"}]}],"member":"320","published-online":{"date-parts":[[2017,3,29]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Spatial interpolants. CoRR abs\/1501.04100","author":"Albarghouthi Aws","year":"2015","unstructured":"Aws Albarghouthi , Josh Berdine , Byron Cook , and Zachary Kincaid . 2015. Spatial interpolants. CoRR abs\/1501.04100 ( 2015 ). Retrieved from http:\/\/arxiv.org\/abs\/1501.04100 Aws Albarghouthi, Josh Berdine, Byron Cook, and Zachary Kincaid. 2015. Spatial interpolants. CoRR abs\/1501.04100 (2015). Retrieved from http:\/\/arxiv.org\/abs\/1501.04100"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_49"},{"key":"e_1_2_1_3_1","unstructured":"Clark Barrett Aaron Stump and Cesare Tinelli. 2010. The Satisfiability Modulo Theories Library (SMT-LIB). (2010). Retrieved from http:\/\/www.smt-lib.org.  Clark Barrett Aaron Stump and Cesare Tinelli. 2010. The Satisfiability Modulo Theories Library (SMT-LIB). (2010). Retrieved from http:\/\/www.smt-lib.org."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_22"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30538-5_9"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0065-2458(03)58003-2"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49059-0_14"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_55"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38856-9_8"},{"key":"e_1_2_1_10_1","volume-title":"The Classical Decision Problem","author":"B\u00f6rger Egon","unstructured":"Egon B\u00f6rger , Erich Gr\u00e4del , and Yuri Gurevich . 2008. The Classical Decision Problem . Springer-Verlag . Egon B\u00f6rger, Erich Gr\u00e4del, and Yuri Gurevich. 2008. The Classical Decision Problem. Springer-Verlag."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04081-8_13"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"e_1_2_1_13_1","volume-title":"Keisler","author":"Chang Chen C.","year":"1990","unstructured":"Chen C. Chang and Howard J . Keisler . 1990 . Model Theory. Elsevier Science . Chen C. Chang and Howard J. Keisler. 1990. Model Theory. Elsevier Science."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_23"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_4"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/775832.775928"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_55"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679392"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/512976.512993"},{"key":"e_1_2_1_20_1","volume-title":"Introduction to Algorithms","author":"Cormen Thomas H.","unstructured":"Thomas H. Cormen , Charles E. Leiserson , Ronald L. Rivest , and Clifford Stein . 2009. Introduction to Algorithms ( 3 rd ed.). The MIT Press . Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. 2009. Introduction to Algorithms (3rd ed.). The MIT Press.","edition":"3"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36126-X_2"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1869459.1869493"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_19"},{"key":"e_1_2_1_26_1","volume-title":"Proceedings of International Conference on Formal Methods in Computer-Aided Design (FMCAD\u201911)","author":"E\u00e9n Niklas","unstructured":"Niklas E\u00e9n , Alan Mishchenko , and Robert K. Brayton . 2011. Efficient implementation of property directed reachability . In Proceedings of International Conference on Formal Methods in Computer-Aided Design (FMCAD\u201911) . FMCAD Inc., 125--134. Niklas E\u00e9n, Alan Mishchenko, and Robert K. Brayton. 2011. Efficient implementation of property directed reachability. In Proceedings of International Conference on Formal Methods in Computer-Aided Design (FMCAD\u201911). FMCAD Inc., 125--134."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45251-6_29"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503291"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-52234-0_12"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/2958031.2958058"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38856-9_11"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-6(4:10)2010"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_3"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31612-8_13"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19835-9_7"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/2958031.2958053"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_3"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_33"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_40"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_2"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297658.1297662"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111048"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328461"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_49"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(80)90027-6"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926455"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23702-7_8"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_13"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378851"},{"key":"e_1_2_1_51_1","volume-title":"The Open Networking Foundation.","author":"ONF.","year":"2016","unstructured":"ONF. 2016. ( 2016 ). The Open Networking Foundation. Retrieved from http:\/\/opennetworking.org. ONF. 2016. (2016). The Open Networking Foundation. Retrieved from http:\/\/opennetworking.org."},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837640"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_47"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_9"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706330"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69738-1_8"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199462"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/514188.514190"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542501"},{"key":"e_1_2_1_61_1","unstructured":"A. Thakur A. Lal J. Lim and T. Reps. 2013. PostHat and All That: Attaining Most-Precise Inductive Invariants. TR-1790. Comp. Sci. Dept. Univ. of Wisconsin\u2014Madison Madison WI.  A. Thakur A. Lal J. Lim and T. Reps. 2013. PostHat and All That: Attaining Most-Precise Inductive Invariants. TR-1790. Comp. Sci. Dept. Univ. of Wisconsin\u2014Madison Madison WI."},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.02.003"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22438-6_36"},{"key":"e_1_2_1_64_1","volume-title":"The Formal Semantics of Programming Languages: An Introduction","author":"Winskel Glynn","unstructured":"Glynn Winskel . 1993. The Formal Semantics of Programming Languages: An Introduction . MIT Press , Cambridge, MA . Glynn Winskel. 1993. The Formal Semantics of Programming Languages: An Introduction. MIT Press, Cambridge, MA."},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_39"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3022187","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3022187","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:23:54Z","timestamp":1750220634000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3022187"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,2,28]]},"references-count":65,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2017,2,28]]}},"alternative-id":["10.1145\/3022187"],"URL":"https:\/\/doi.org\/10.1145\/3022187","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,2,28]]},"assertion":[{"value":"2016-01-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2016-12-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-03-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}