{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,24]],"date-time":"2026-06-24T15:02:30Z","timestamp":1782313350331,"version":"3.54.5"},"reference-count":46,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2014,9,5]],"date-time":"2014-09-05T00:00:00Z","timestamp":1409875200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000144","name":"Division of Computer and Network Systems","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100000144","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100011419","name":"Santa Fe Institute","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100011419","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100000143","name":"Division of Computing and Communication Foundations","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100000143","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000015","name":"U.S. Department of Energy","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100000015","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2014,9,5]]},"abstract":"<jats:p>This article describes and evaluates DIG, a dynamic invariant generator that infers invariants from observed program traces, focusing on numerical and array variables. For numerical invariants, DIG supports both nonlinear equalities and inequalities of arbitrary degree defined over numerical program variables. For array invariants, DIG generates nested relations among multidimensional array variables. These properties are nontrivial and challenging for current static and dynamic invariant analysis methods. The key difference between DIG and existing dynamic methods is its generative technique, which infers invariants directly from traces, instead of using traces to filter out predefined templates. To generate accurate invariants, DIG employs ideas and tools from the mathematical and formal methods domains, including equation solving, polyhedra construction, and theorem proving; for example, DIG represents and reasons about polynomial invariants using geometric shapes. Experimental results on 27 mathematical algorithms and an implementation of AES encryption provide evidence that DIG is effective at generating invariants for these programs.<\/jats:p>","DOI":"10.1145\/2556782","type":"journal-article","created":{"date-parts":[[2014,9,9]],"date-time":"2014-09-09T10:39:29Z","timestamp":1410259169000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":38,"title":["DIG"],"prefix":"10.1145","volume":"23","author":[{"given":"Thanhvu","family":"Nguyen","sequence":"first","affiliation":[{"name":"University of New Mexico"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Deepak","family":"Kapur","sequence":"additional","affiliation":[{"name":"University of New Mexico"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Westley","family":"Weimer","sequence":"additional","affiliation":[{"name":"University of Virginia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Stephanie","family":"Forrest","sequence":"additional","affiliation":[{"name":"University of New Mexico"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2014,9,5]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/829555"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781153"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349342"},{"key":"e_1_2_1_4_1","unstructured":"Enric Rodr\u00edguez Carbonell. 2006. Automatic generation of polynomial invariants for system verification. Ph.D. Dissertation Technical University of Catalonia Barcelona Spain."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2007.01.002"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","unstructured":"Enric Rodr\u00edguez Carbonell and D. Kapur. 2007b. Automatic generation of polynomial invariants of bounded degree using abstract interpretation. Sci. Comput. Program. 64. (Jan. 2007) 54--75. DOI: http:\/\/dx.doi.org\/10.1016\/j.scico.2006.03.003 10.1016\/j.scico.2006.03.003","DOI":"10.1016\/j.scico.2006.03.003"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/91408"},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the International Symposium on Programming. 106--130","author":"Cousot P.","unstructured":"P. Cousot and R. Cousot. 1976. Static determination of dynamic properties of programs. In Proceedings of the International Symposium on Programming. 106--130."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_3"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_3"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/261226"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/800099.803206"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_11"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/932221"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","unstructured":"Michael D. Ernst Jeff H. Perkins Philip J. Guo Stephen McCamant Carlos Pacheco Matthew S. Tschantz and Chen Xiao. 2007. The Daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 1--3. (2007) 35--45. 10.1016\/j.scico.2007.01.015","DOI":"10.1016\/j.scico.2007.01.015"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/59113"},{"key":"e_1_2_1_20_1","volume-title":"Programming Languages and Systems","author":"Feret J\u00e9r\u00f4me","unstructured":"J\u00e9r\u00f4me Feret. 2004. Static analysis of digital filters. In Programming Languages and Systems, Springer, 33--48."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/647540.730008"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1975.6312821"},{"key":"e_1_2_1_23_1","volume-title":"Proceedings of the International Conference on Automated Software Engineering. 49--58","author":"Gupta N.","unstructured":"N. Gupta and Z. V. Heidepriem. 2003. A new structural coverage criterion for dynamic detection of program invariants. In Proceedings of the International Conference on Automated Software Engineering. 49--58."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/581339.581377"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/776816.776824"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/153676"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268497"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/360032.360048"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065014"},{"key":"e_1_2_1_30_1","unstructured":"Antoine Min\u00e9. 2004. Weakly relational numerical abstract domains. Ph.D. Dissertation \u00c9cole Polytechnique Palaiseau France."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/2337223.2337304"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/648230.752639"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1041685.1029901"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629585"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199462"},{"key":"e_1_2_1_36_1","unstructured":"V. Rijmen and J. Daemen. 2001. Advanced encryption standard. Federal Information Processing Standards Publications National Institute of Standards and Technology (2001) 19--22."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31954-2_39"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_2"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_31"},{"key":"e_1_2_1_40_1","volume-title":"Mathematics Software","author":"Stein W.A.","unstructured":"W.A. Stein. 2012. Mathematics Software. Sage. http:\/\/www.sagemath.org."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512963"},{"key":"e_1_2_1_42_1","volume-title":"Proceedings of the SPIN Model Checking and Software Verification Workshop.","author":"Vaziri M.","unstructured":"M. Vaziri and G. Holzmann. 1998. Automatic detection of invariants in Spin. In Proceedings of the SPIN Model Checking and Software Verification Workshop."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/360827.360850"},{"key":"e_1_2_1_44_1","volume-title":"Proceedings of the International Conference on Automated Software Engineering. 40--48","author":"Xie T.","unstructured":"T. Xie and D. Notkin. 2003. Tool-assisted unit test selection based on operational violations. In Proceedings of the International Conference on Automated Software Engineering. 40--48."},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87698-4_26"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2009.5270355"}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2556782","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2556782","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2556782","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T09:45:28Z","timestamp":1763459128000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2556782"}},"subtitle":["A Dynamic Invariant Generator for Polynomial and Array Invariants"],"short-title":[],"issued":{"date-parts":[[2014,9,5]]},"references-count":46,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2014,9,5]]}},"alternative-id":["10.1145\/2556782"],"URL":"https:\/\/doi.org\/10.1145\/2556782","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"value":"1049-331X","type":"print"},{"value":"1557-7392","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,9,5]]},"assertion":[{"value":"2012-12-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-11-01","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-09-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}