{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,13]],"date-time":"2026-05-13T02:00:33Z","timestamp":1778637633145,"version":"3.51.4"},"publisher-location":"New York, NY, USA","reference-count":38,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,8,21]],"date-time":"2017-08-21T00:00:00Z","timestamp":1503273600000},"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":[[2017,8,21]]},"DOI":"10.1145\/3106237.3106281","type":"proceedings-article","created":{"date-parts":[[2017,8,2]],"date-time":"2017-08-02T19:36:18Z","timestamp":1501702578000},"page":"605-615","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":39,"title":["Counterexample-guided approach to finding numerical invariants"],"prefix":"10.1145","author":[{"given":"ThanhVu","family":"Nguyen","sequence":"first","affiliation":[{"name":"University of Nebraska-Lincoln, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Timos","family":"Antonopoulos","sequence":"additional","affiliation":[{"name":"Yale University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew","family":"Ruef","sequence":"additional","affiliation":[{"name":"University of Maryland, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Hicks","sequence":"additional","affiliation":[{"name":"University of Maryland, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,8,21]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062378"},{"key":"e_1_3_2_1_2_1","volume-title":"Rajamani","author":"Ball Thomas","year":"2001","unstructured":"Thomas Ball and Sriram K . Rajamani . 2001 . Automatically Validating Temporal Safety Properties of Interfaces. In SPIN Symposium on Model Checking of Software. Springer , 103\u2013122. Thomas Ball and Sriram K. Rajamani. 2001. Automatically Validating Temporal Safety Properties of Interfaces. In SPIN Symposium on Model Checking of Software. Springer, 103\u2013122."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54580-5_20"},{"key":"e_1_3_2_1_4_1","volume-title":"CPAchecker: A Tool for Configurable Software Verification","author":"Beyer Dirk","unstructured":"Dirk Beyer and M. Erkan Keremoglu . 2011. CPAchecker: A Tool for Configurable Software Verification . In CAV. Springer , 184\u2013190. Dirk Beyer and M. Erkan Keremoglu. 2011. CPAchecker: A Tool for Configurable Software Verification. In CAV. Springer, 184\u2013190."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781153"},{"key":"e_1_3_2_1_6_1","volume-title":"OSDI","volume":"8","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar , Daniel Dunbar , and Dawson R Engler . 2008 . KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs .. In OSDI , Vol. 8 . USENIX Association, 209\u2013224. Cristian Cadar, Daniel Dunbar, and Dawson R Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs.. In OSDI, Vol. 8. USENIX Association, 209\u2013224."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2007.01.002"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"crossref","unstructured":"E. Clarke O. Grumberg S. Jha Y. Lu and H. Veith. 2000. Counterexample-guided abstraction refinement. In CAV. Springer 154\u2013169.   E. Clarke O. Grumberg S. Jha Y. Lu and H. Veith. 2000. Counterexample-guided abstraction refinement. In CAV. Springer 154\u2013169.","DOI":"10.1007\/10722167_15"},{"key":"e_1_3_2_1_10_1","volume-title":"Programming in the 1990s: An introduction to the calculation of programs","author":"Cohen Edward","unstructured":"Edward Cohen . 1990. Programming in the 1990s: An introduction to the calculation of programs . Springer . Edward Cohen. 1990. Programming in the 1990s: An introduction to the calculation of programs. Springer."},{"key":"e_1_3_2_1_11_1","volume-title":"Static Determination of Dynamic Properties of Programs. In International Symposium on Programming. 106\u2013130","author":"Cousot P.","unstructured":"P. Cousot and R. Cousot . 1976 . Static Determination of Dynamic Properties of Programs. In International Symposium on Programming. 106\u2013130 . P. Cousot and R. Cousot. 1976. Static Determination of Dynamic Properties of Programs. In International Symposium on Programming. 106\u2013130."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_1_13_1","volume-title":"The Astr\u00e9e analyzer","author":"Cousot Patrick","unstructured":"Patrick Cousot , Radhia Cousot , Jer\u00f4me Feret , Laurent Mauborgne , Antoine Min\u00e9 , David Monniaux , and Xavier Rival . 2005. The Astr\u00e9e analyzer . In ESOP. Springer , 21\u201330. Patrick Cousot, Radhia Cousot, Jer\u00f4me Feret, Laurent Mauborgne, Antoine Min\u00e9, David Monniaux, and Xavier Rival. 2005. The Astr\u00e9e analyzer. In ESOP. Springer, 21\u201330."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512538"},{"key":"e_1_3_2_1_16_1","volume-title":"Z3: An efficient SMT solver","author":"Moura Leonardo De","unstructured":"Leonardo De Moura and Nikolaj Bj\u00f8rner . 2008. Z3: An efficient SMT solver . In TACAS. Springer , 337\u2013340. Leonardo De Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An efficient SMT solver. In TACAS. Springer, 337\u2013340."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509511"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.908957"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/337180.337240"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.01.015"},{"key":"e_1_3_2_1_22_1","volume-title":"Static analysis of digital filters","author":"Feret J\u00e9r\u00f4me","unstructured":"J\u00e9r\u00f4me Feret . 2004. Static analysis of digital filters . In ESOP. Springer , 33\u201348. J\u00e9r\u00f4me Feret. 2004. Static analysis of digital filters. In ESOP. Springer, 33\u201348."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837664"},{"key":"e_1_3_2_1_24_1","volume-title":"JPF: Java PathFinder.","author":"The Java","year":"2017","unstructured":"The Java Pathfinder group. 2017 . JPF: Java PathFinder. (2017). http:\/\/babelfish. arc.nasa.gov\/trac\/jpf\/. The Java Pathfinder group. 2017. JPF: Java PathFinder. (2017). http:\/\/babelfish. arc.nasa.gov\/trac\/jpf\/."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_7"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542518"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480898"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706353"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_64"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_3_2_1_33_1","volume-title":"Verifying and Synthesizing Constant-Resource Implementations with Types. In 2017 IEEE Symposium on Security and Privacy. 710\u2013728","author":"Ngo Van Chan","year":"2017","unstructured":"Van Chan Ngo , Mario Dehesa-Azuara , Matthew Fredrikson , and Jan Hoffmann . 2017 . Verifying and Synthesizing Constant-Resource Implementations with Types. In 2017 IEEE Symposium on Security and Privacy. 710\u2013728 . Van Chan Ngo, Mario Dehesa-Azuara, Matthew Fredrikson, and Jan Hoffmann. 2017. Verifying and Synthesizing Constant-Resource Implementations with Types. In 2017 IEEE Symposium on Security and Privacy. 710\u2013728."},{"key":"e_1_3_2_1_35_1","volume-title":"Using Dynamic Analysis to Discover Polynomial and Array Invariants","author":"Nguyen ThanhVu","unstructured":"ThanhVu Nguyen , Deepak Kapur , Westley Weimer , and Stephanie Forrest . 2012. Using Dynamic Analysis to Discover Polynomial and Array Invariants . In ICSE. IEEE , 683\u2013693. ThanhVu Nguyen, Deepak Kapur, Westley Weimer, and Stephanie Forrest. 2012. Using Dynamic Analysis to Discover Polynomial and Array Invariants. In ICSE. IEEE, 683\u2013693."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2556782"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908099"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1029894.1029901"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2006.03.003"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31954-2_39"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_2"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_31"}],"event":{"name":"ESEC\/FSE'17: Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering","location":"Paderborn Germany","acronym":"ESEC\/FSE'17","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3106237.3106281","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3106237.3106281","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:30:37Z","timestamp":1750217437000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3106237.3106281"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,8,21]]},"references-count":38,"alternative-id":["10.1145\/3106237.3106281","10.1145\/3106237"],"URL":"https:\/\/doi.org\/10.1145\/3106237.3106281","relation":{},"subject":[],"published":{"date-parts":[[2017,8,21]]},"assertion":[{"value":"2017-08-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}