{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:58:02Z","timestamp":1776333482286,"version":"3.51.2"},"publisher-location":"New York, NY, USA","reference-count":31,"publisher":"ACM","license":[{"start":{"date-parts":[[2012,11,11]],"date-time":"2012-11-11T00:00:00Z","timestamp":1352592000000},"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":[[2012,11,11]]},"DOI":"10.1145\/2393596.2393665","type":"proceedings-article","created":{"date-parts":[[2012,11,13]],"date-time":"2012-11-13T15:04:07Z","timestamp":1352819047000},"page":"1-11","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":120,"title":["Green"],"prefix":"10.1145","author":[{"given":"Willem","family":"Visser","sequence":"first","affiliation":[{"name":"Stellenbosch University, Stellenbosch, South Africa"}]},{"given":"Jaco","family":"Geldenhuys","sequence":"additional","affiliation":[{"name":"Stellenbosch University, Stellenbosch, South Africa"}]},{"given":"Matthew B.","family":"Dwyer","sequence":"additional","affiliation":[{"name":"University of Nebraska - Lincoln, Lincoln, NE"}]}],"member":"320","published-online":{"date-parts":[[2012,11,11]]},"reference":[{"key":"e_1_3_2_1_1_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"298","DOI":"10.1007\/978-3-540-73368-3_34","volume-title":"Proceedings of the 19th International Conference on Computer Aided Verification (CAV '07)","author":"Barrett C.","year":"2007","unstructured":"C. Barrett and C. Tinelli . CVC3 . In W. Damm and H. Hermanns, editors, Proceedings of the 19th International Conference on Computer Aided Verification (CAV '07) , volume 4590 of Lecture Notes in Computer Science , pages 298 -- 302 . Springer-Verlag , July 2007 . Berlin, Germany. C. Barrett and C. Tinelli. CVC3. In W. Damm and H. Hermanns, editors, Proceedings of the 19th International Conference on Computer Aided Verification (CAV '07), volume 4590 of Lecture Notes in Computer Science, pages 298--302. Springer-Verlag, July 2007. Berlin, Germany."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1646353.1646374"},{"key":"e_1_3_2_1_3_1","first-page":"209","volume-title":"Proceedings of the 8th USENIX conference on Operating systems design and implementation, OSDI'08","author":"Cadar C.","year":"2008","unstructured":"C. Cadar , D. Dunbar , and D. Engler . Klee: unassisted and automatic generation of high-coverage tests for complex systems programs . In Proceedings of the 8th USENIX conference on Operating systems design and implementation, OSDI'08 , pages 209 -- 224 , Berkeley, CA, USA , 2008 . USENIX Association. C. Cadar, D. Dunbar, and D. Engler. Klee: unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th USENIX conference on Operating systems design and implementation, OSDI'08, pages 209--224, Berkeley, CA, USA, 2008. USENIX Association."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1455518.1455522"},{"key":"e_1_3_2_1_5_1","unstructured":"Choco. Choco Solver. http:\/\/www.emn.fr\/z-info\/choco-solver\/.  Choco. Choco Solver. http:\/\/www.emn.fr\/z-info\/choco-solver\/."},{"key":"e_1_3_2_1_6_1","volume-title":"Introduction to Algorithms","author":"Cormen T. H.","year":"2001","unstructured":"T. H. Cormen , C. Stein , R. L. Rivest , and C. E. Leiserson . Introduction to Algorithms . McGraw-Hill Higher Education , 2001 . T. H. Cormen, C. Stein, R. L. Rivest, and C. E. Leiserson. Introduction to Algorithms. McGraw-Hill Higher Education, 2001."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"crossref","first-page":"218","DOI":"10.1007\/978-3-540-25984-8_14","volume-title":"Automated Reasoning","author":"de Moura L.","year":"2004","unstructured":"L. de Moura , S. Owre , H. Rue\u00c3 §, J. Rushby , and N. Shankar . The ICS decision procedures for embedded deduction . In Automated Reasoning , volume 3097 , pages 218 -- 222 . Springer , 2004 . L. de Moura, S. Owre, H. Rue\u00c3§, J. Rushby, and N. Shankar. The ICS decision procedures for embedded deduction. In Automated Reasoning, volume 3097, pages 218--222. Springer, 2004."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.06.068"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.92910"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2338965.2336773"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2093548.2093564"},{"key":"e_1_3_2_1_12_1","volume-title":"International Journal on Software Tools for Technology Transfer (STTT), 6:302--319","author":"Iosif R.","year":"2004","unstructured":"R. Iosif . Symmetry reductions for model checking of concurrent dynamic software . International Journal on Software Tools for Technology Transfer (STTT), 6:302--319 , 2004 . R. Iosif. Symmetry reductions for model checking of concurrent dynamic software. International Journal on Software Tools for Technology Transfer (STTT), 6:302--319, 2004."},{"key":"e_1_3_2_1_13_1","unstructured":"Jedis. Redis Java Interface. http:\/\/code.google.com\/p\/jedis\/.  Jedis. Redis Java Interface. http:\/\/code.google.com\/p\/jedis\/."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2010.62"},{"key":"e_1_3_2_1_15_1","unstructured":"Jumble. Jumble mutation testing tool. http:\/\/jumble.sourceforge.net\/.  Jumble. Jumble mutation testing tool. http:\/\/jumble.sourceforge.net\/."},{"key":"e_1_3_2_1_16_1","unstructured":"LattE. LattE Integrale UC Davis Mathematics. http:\/\/www.math.ucdavis.edu\/~latte.  LattE. LattE Integrale UC Davis Mathematics. http:\/\/www.math.ucdavis.edu\/~latte."},{"key":"e_1_3_2_1_17_1","volume-title":"Art of Software Testing","author":"Myers G. J.","year":"1979","unstructured":"G. J. Myers . Art of Software Testing . John Wiley & Sons, Inc. , 1979 . G. J. Myers. Art of Software Testing. John Wiley & Sons, Inc., 1979."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/357073.357079"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1453101.1453131"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993558"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1858996.1859035"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032360"},{"key":"e_1_3_2_1_23_1","unstructured":"Redis. Redis NoSQL Database. http:\/\/redis.io.  Redis. Redis NoSQL Database. http:\/\/redis.io."},{"key":"e_1_3_2_1_24_1","volume-title":"Proceedings of the Seventh International Conference on Theory and Applications of Satisfiability Testing","author":"Sang T.","year":"2004","unstructured":"T. Sang , F. Bacchus , P. Beame , H. A. Kautz , and T. Pitassi . Combining component caching and clause learning for effective model counting . In Proceedings of the Seventh International Conference on Theory and Applications of Satisfiability Testing , 2004 . T. Sang, F. Bacchus, P. Beame, H. A. Kautz, and T. Pitassi. Combining component caching and clause learning for effective model counting. In Proceedings of the Seventh International Conference on Theory and Applications of Satisfiability Testing, 2004."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146238.1146256"},{"key":"e_1_3_2_1_26_1","unstructured":"SIR. SIR Repository. http:\/\/sir.unl.edu.  SIR. SIR Repository. http:\/\/sir.unl.edu."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792786.1792798"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146238.1146243"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2338965.2336771"},{"key":"e_1_3_2_1_30_1","unstructured":"Yikes. Yices SMT Solver. http:\/\/yices.csl.sri.com\/.  Yikes. Yices SMT Solver. http:\/\/yices.csl.sri.com\/."},{"key":"e_1_3_2_1_31_1","volume-title":"SAT Research Group","unstructured":"zChaff. SAT Research Group , Princeton University . http:\/\/www.princeton.edu\/~chaff\/zchaff.html. zChaff. SAT Research Group, Princeton University. http:\/\/www.princeton.edu\/~chaff\/zchaff.html."}],"event":{"name":"SIGSOFT\/FSE'12: 20th ACM SIGSOFT Symposium on the Foundations of Software Engineering","location":"Cary North Carolina","acronym":"SIGSOFT\/FSE'12","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2393596.2393665","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2393596.2393665","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T09:34:56Z","timestamp":1750239296000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2393596.2393665"}},"subtitle":["reducing, reusing and recycling constraints in program analysis"],"short-title":[],"issued":{"date-parts":[[2012,11,11]]},"references-count":31,"alternative-id":["10.1145\/2393596.2393665","10.1145\/2393596"],"URL":"https:\/\/doi.org\/10.1145\/2393596.2393665","relation":{},"subject":[],"published":{"date-parts":[[2012,11,11]]},"assertion":[{"value":"2012-11-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}