{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:16:33Z","timestamp":1763468193441,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":41,"publisher":"ACM","license":[{"start":{"date-parts":[[2014,5,31]],"date-time":"2014-05-31T00:00:00Z","timestamp":1401494400000},"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":[[2014,5,31]]},"DOI":"10.1145\/2568225.2568275","type":"proceedings-article","created":{"date-parts":[[2014,5,20]],"date-time":"2014-05-20T13:48:00Z","timestamp":1400593680000},"page":"608-619","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":28,"title":["Using dynamic analysis to generate disjunctive invariants"],"prefix":"10.1145","author":[{"given":"ThanhVu","family":"Nguyen","sequence":"first","affiliation":[{"name":"University of New Mexico, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Deepak","family":"Kapur","sequence":"additional","affiliation":[{"name":"University of New Mexico, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Westley","family":"Weimer","sequence":"additional","affiliation":[{"name":"University of Virginia, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephanie","family":"Forrest","sequence":"additional","affiliation":[{"name":"University of New Mexico, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2014,5,31]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69166-2_13"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcta.2013.01.011"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/380921.380932"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781153"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2007.01.002"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00237-2"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_3"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_3"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_3_2_1_12_1","first-page":"438","volume-title":"Discrete Event Systems, 2006 8th International Workshop on","author":"Daniel-Cavalcante M.","unstructured":"M. Daniel-Cavalcante , M. F. Magalhaes , and R. Santos-Mendes . The max-plus algebra and the network calculus . In Discrete Event Systems, 2006 8th International Workshop on , pages 433\u2013 438 . IEEE, 2006. M. Daniel-Cavalcante, M. F. Magalhaes, and R. Santos-Mendes. The max-plus algebra and the network calculus. In Discrete Event Systems, 2006 8th International Workshop on, pages 433\u2013438. IEEE, 2006."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/543552.512538"},{"key":"e_1_3_2_1_14_1","first-page":"340","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"De Moura L.","unstructured":"L. De Moura and N. Bj\u00f8rner . Z3: An e\ufb03cient SMT solver . In Tools and Algorithms for the Construction and Analysis of Systems , pages 337\u2013 340 . Springer, 2008. http:\/\/research.microsoft.com\/en-us\/um\/ redmond\/projects\/z3\/. L. De Moura and N. Bj\u00f8rner. Z3: An e\ufb03cient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems, pages 337\u2013340. Springer, 2008. http:\/\/research.microsoft.com\/en-us\/um\/ redmond\/projects\/z3\/."},{"key":"e_1_3_2_1_15_1","volume-title":"Extended static checking","author":"Detlefs D. L.","year":"1998","unstructured":"D. L. Detlefs , K. R. M. Leino , G. Nelson , and J. B. Saxe . Extended static checking . 1998 . D. L. Detlefs, K. R. M. Leino, G. Nelson, and J. B. Saxe. Extended static checking. 1998."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/2041552.2041578"},{"key":"e_1_3_2_1_18_1","first-page":"02","article-title":"Dynamically discovering program invariants involving collections. University of Washington","volume":"99","author":"Ernst M. D.","year":"2000","unstructured":"M. D. Ernst , W. G. Griswold , Y. Kataoka , and D. Notkin . Dynamically discovering program invariants involving collections. University of Washington , TR UW-CSE- 99-11 - 02 , 2000 . M. D. Ernst, W. G. Griswold, Y. Kataoka, and D. Notkin. Dynamically discovering program invariants involving collections. University of Washington, TR UW-CSE-99-11-02, 2000.","journal-title":"TR UW-CSE-"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.01.015"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190258"},{"key":"e_1_3_2_1_21_1","volume-title":"Max Plus at work: modeling and analysis of synchronized systems: a course on Max-Plus algebra and its applications","author":"Heidergott B.","year":"2006","unstructured":"B. Heidergott and J. W. van der Woude . Max Plus at work: modeling and analysis of synchronized systems: a course on Max-Plus algebra and its applications , volume 13 . Princeton University Press , 2006 . B. Heidergott and J. W. van der Woude. Max Plus at work: modeling and analysis of synchronized systems: a course on Max-Plus algebra and its applications, volume 13. Princeton University Press, 2006."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"e_1_3_2_1_23_1","unstructured":"B. Jeannet. Interproc analyzer for recursive programs with numerical variables. INRIA software and documentation are available at the following URL: http:\/\/pop-art. inrialpes. fr\/interproc\/interprocweb. cgi. Last accessed pages 06\u201311 2010.  B. Jeannet. Interproc analyzer for recursive programs with numerical variables. INRIA software and documentation are available at the following URL: http:\/\/pop-art. inrialpes. fr\/interproc\/interprocweb. cgi. Last accessed pages 06\u201311 2010."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31365-3_27"},{"key":"e_1_3_2_1_25_1","first-page":"206","volume-title":"NASA Formal Methods","author":"Kahsai T.","unstructured":"T. Kahsai , Y. Ge , and C. Tinelli . Instantiation-based invariant discovery . In NASA Formal Methods , pages 192\u2013 206 . Springer, 2011. T. Kahsai, Y. Ge, and C. Tinelli. Instantiation-based invariant discovery. In NASA Formal Methods, pages 192\u2013206. Springer, 2011."},{"key":"e_1_3_2_1_26_1","first-page":"62","volume-title":"Proceedings of 10th International Workshop on Parallel and Distributed Methods in verifiCation (Snowbird, Utah, USA), Electronic Proceedings in Theoretical Computer Science","author":"Kahsai T.","year":"2011","unstructured":"T. Kahsai and C. Tinelli . PKIND: a parallel k-induction based model checker. In J. Barnat and K. Heljanko, editors , Proceedings of 10th International Workshop on Parallel and Distributed Methods in verifiCation (Snowbird, Utah, USA), Electronic Proceedings in Theoretical Computer Science , pages 55\u2013 62 , 2011 . T. Kahsai and C. Tinelli. PKIND: a parallel k-induction based model checker. In J. Barnat and K. Heljanko, editors, Proceedings of 10th International Workshop on Parallel and Distributed Methods in verifiCation (Snowbird, Utah, USA), Electronic Proceedings in Theoretical Computer Science, pages 55\u201362, 2011."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/2554473.2554484"},{"key":"e_1_3_2_1_28_1","first-page":"178","article-title":"This is Boogie 2","author":"Leino K. R. M.","year":"2008","unstructured":"K. R. M. Leino . This is Boogie 2 . Manuscript KRML , 178 , 2008 . K. R. M. Leino. This is Boogie 2. Manuscript KRML, 178, 2008.","journal-title":"Manuscript KRML"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_3_2_1_31_1","first-page":"693","volume-title":"International Conference on Software Engineering","author":"Nguyen T.","unstructured":"T. Nguyen , D. Kapur , W. Weimer , and S. Forrest . Using Dynamic Analysis to Discover Polynomial and Array Invariants . In International Conference on Software Engineering , pages 683\u2013 693 . IEEE, 2012. T. Nguyen, D. Kapur, W. Weimer, and S. Forrest. Using Dynamic Analysis to Discover Polynomial and Array Invariants. In International Conference on Software Engineering, pages 683\u2013693. IEEE, 2012."},{"key":"e_1_3_2_1_32_1","volume-title":"DIG: A Dynamic Invariant Generator for Polynomial and Array Invariants. ACM Transactions on Software Engineering and Methodology, to appear","author":"Nguyen T.","year":"2014","unstructured":"T. Nguyen , D. Kapur , W. Weimer , and S. Forrest . DIG: A Dynamic Invariant Generator for Polynomial and Array Invariants. ACM Transactions on Software Engineering and Methodology, to appear , 2014 . T. Nguyen, D. Kapur, W. Weimer, and S. Forrest. DIG: A Dynamic Invariant Generator for Polynomial and Array Invariants. ACM Transactions on Software Engineering and Methodology, to appear, 2014."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)00256-7"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/566172.566213"},{"key":"e_1_3_2_1_35_1","first-page":"80","volume-title":"Formal Methods in Computer-Aided Design","author":"Nuzzo P.","year":"2010","unstructured":"P. Nuzzo , A. Puggelli , S. A. Seshia , and A. Sangiovanni-Vincentelli . CalCS: SMT solving for non-linear convex constraints . In Formal Methods in Computer-Aided Design , pages 71\u2013 80 , 2010 . P. Nuzzo, A. Puggelli, S. A. Seshia, and A. Sangiovanni-Vincentelli. CalCS: SMT solving for non-linear convex constraints. In Formal Methods in Computer-Aided Design, pages 71\u201380, 2010."},{"key":"e_1_3_2_1_36_1","first-page":"345","volume-title":"Advances in Computer Science-ASIAN","author":"Popeea C.","year":"2006","unstructured":"C. Popeea and W.-N. Chin . Inferring disjunctive postconditions . In Advances in Computer Science-ASIAN 2006 . Secure Software and Related Issues , pages 331\u2013 345 . Springer, 2007. C. Popeea and W.-N. Chin. Inferring disjunctive postconditions. In Advances in Computer Science-ASIAN 2006. Secure Software and Related Issues, pages 331\u2013345. Springer, 2007."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2006.03.003"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/11823230_2"},{"key":"e_1_3_2_1_39_1","first-page":"411","volume-title":"Static Analysis","author":"Sharma R.","unstructured":"R. Sharma , S. Gupta , B. Hariharan , A. Aiken , and A. V. Nori . Verification as learning geometric concepts . In Static Analysis , pages 388\u2013 411 . Springer, 2013. R. Sharma, S. Gupta, B. Hariharan, A. Aiken, and A. V. Nori. Verification as learning geometric concepts. In Static Analysis, pages 388\u2013411. Springer, 2013."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.5555\/646186.683237"},{"key":"e_1_3_2_1_41_1","volume-title":"Sage Mathematics Software","author":"Stein W.","year":"2012","unstructured":"W. Stein Sage Mathematics Software , 2012 . http:\/\/www.sagemath.org. W. Stein et al. Sage Mathematics Software, 2012. http:\/\/www.sagemath.org."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1831708.1831716"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1173706.1173734"}],"event":{"name":"ICSE '14: 36th International Conference on Software Engineering","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","TCSE IEEE Computer Society's Tech. Council on Software Engin."],"location":"Hyderabad India","acronym":"ICSE '14"},"container-title":["Proceedings of the 36th International Conference on Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2568225.2568275","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2568225.2568275","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:10:30Z","timestamp":1750234230000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2568225.2568275"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,5,31]]},"references-count":41,"alternative-id":["10.1145\/2568225.2568275","10.1145\/2568225"],"URL":"https:\/\/doi.org\/10.1145\/2568225.2568275","relation":{},"subject":[],"published":{"date-parts":[[2014,5,31]]},"assertion":[{"value":"2014-05-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}