{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:47:48Z","timestamp":1772164068144,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":34,"publisher":"ACM","license":[{"start":{"date-parts":[[2014,10,15]],"date-time":"2014-10-15T00:00:00Z","timestamp":1413331200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100003074","name":"Agencia Nacional de Promoci\u00f3n Cient\u00edfica y Tecnol\u00f3gica","doi-asserted-by":"publisher","award":["2012-1298"],"award-info":[{"award-number":["2012-1298"]}],"id":[{"id":"10.13039\/501100003074","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003074","name":"Agencia Nacional de Promoci\u00f3n Cient\u00edfica y Tecnol\u00f3gica","doi-asserted-by":"publisher","award":["PICT 2010-1690"],"award-info":[{"award-number":["PICT 2010-1690"]}],"id":[{"id":"10.13039\/501100003074","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100005363","name":"Universidad de Buenos Aires","doi-asserted-by":"publisher","award":["ITBACyT 8"],"award-info":[{"award-number":["ITBACyT 8"]}],"id":[{"id":"10.13039\/501100005363","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004963","name":"Seventh Framework Programme","doi-asserted-by":"publisher","award":["EU FP7 MEALS - 295261"],"award-info":[{"award-number":["EU FP7 MEALS - 295261"]}],"id":[{"id":"10.13039\/501100004963","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000143","name":"Division of Computing and Communication Foundations","doi-asserted-by":"publisher","award":["CCF-0845628"],"award-info":[{"award-number":["CCF-0845628"]}],"id":[{"id":"10.13039\/100000143","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000144","name":"Division of Computer and Network Systems","doi-asserted-by":"publisher","award":["CNS-1239498"],"award-info":[{"award-number":["CNS-1239498"]}],"id":[{"id":"10.13039\/100000144","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2014,10,15]]},"DOI":"10.1145\/2660193.2660232","type":"proceedings-article","created":{"date-parts":[[2014,10,21]],"date-time":"2014-10-21T08:59:05Z","timestamp":1413881945000},"page":"655-674","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Bounded exhaustive test input generation from hybrid invariants"],"prefix":"10.1145","author":[{"given":"Nicol\u00e1s","family":"Rosner","sequence":"first","affiliation":[{"name":"University of Buenos Aires, Buenos Aires, Argentina"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Valeria","family":"Bengolea","sequence":"additional","affiliation":[{"name":"University of Rio Cuarto, Rio Cuarto, Argentina"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pablo","family":"Ponzio","sequence":"additional","affiliation":[{"name":"University of Rio Cuarto, Rio Cuarto, Argentina"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shadi Abdul","family":"Khalek","sequence":"additional","affiliation":[{"name":"Google, Kirkland, WA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nazareno","family":"Aguirre","sequence":"additional","affiliation":[{"name":"University of Rio Cuarto & CONICET, Rio Cuarto, Argentina"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marcelo F.","family":"Frias","sequence":"additional","affiliation":[{"name":"Buenos Aires Institute of Technology & CONICET, Buenos Aires, Argentina"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sarfraz","family":"Khurshid","sequence":"additional","affiliation":[{"name":"The University of Texas at Austin, Austin, TX, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2014,10,15]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2013.46"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/566172.566191"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0167-4"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1134285.1134329"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351266"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146238.1146251"},{"key":"e_1_3_2_1_8_1","volume-title":"The Yices SMT solver. Technical report","author":"Dutertre B.","year":"2006","unstructured":"B. Dutertre and L. D. Moura . The Yices SMT solver. Technical report , 2006 . B. Dutertre and L. D. Moura. The Yices SMT solver. Technical report, 2006."},{"key":"e_1_3_2_1_9_1","volume-title":"An Extensible SAT-solver. In SAT","author":"Een N.","year":"2003","unstructured":"N. Een and N. Sorensson . An Extensible SAT-solver. In SAT 2003 . N. Een and N. Sorensson. An Extensible SAT-solver. In SAT 2003."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1062455.1062535"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2013.15"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34281-3_29"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38088-4_16"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806799.1806835"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_3_2_1_16_1","volume-title":"Software Abstractions: Logic, Language and Analysis","author":"Jackson D.","year":"2006","unstructured":"D. Jackson , Software Abstractions: Logic, Language and Analysis , The MIT Press , 2006 . D. Jackson, Software Abstractions: Logic, Language and Analysis, The MIT Press, 2006."},{"key":"e_1_3_2_1_17_1","volume-title":"Lessons Learned in Software Testing","author":"Kaner C.","year":"2001","unstructured":"C. Kaner , J. Bach and B. Pettichord , Lessons Learned in Software Testing , Wiley , 2001 . C. Kaner, J. Bach and B. Pettichord, Lessons Learned in Software Testing, Wiley, 2001."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2011.6100122"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2011.6100137"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:AUSE.0000038938.10589.b9"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103675"},{"key":"e_1_3_2_1_23_1","volume-title":"Program Development in Java: Abstraction, Specification, and Object-Oriented Design","author":"Liskov B.","year":"2000","unstructured":"B. Liskov and J. Guttag , Program Development in Java: Abstraction, Specification, and Object-Oriented Design , Addison-Wesley , 2000 . B. Liskov and J. Guttag, Program Development in Java: Abstraction, Specification, and Object-Oriented Design, Addison-Wesley, 2000."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2007.48"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985863"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2007.37"},{"key":"e_1_3_2_1_27_1","volume-title":"VSTTE 2014","author":"Rosner N.","year":"2013","unstructured":"N. Rosner , C. G. L\u00f3pez Pombo , N. Aguirre , A. Jaoua , A. Mili and M. F. Frias , Parallel Bounded Verification of Alloy Models by TranScoping , in VSTTE 2014 , LNCS, Springer , 2013 . N. Rosner, C. G. L\u00f3pez Pombo, N. Aguirre, A. Jaoua, A. Mili and M. F. Frias, Parallel Bounded Verification of Alloy Models by TranScoping, in VSTTE 2014, LNCS, Springer, 2013."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/1883978.1884015"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10373-5_5"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_22"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1007512.1007526"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/1025115.1025219"},{"key":"e_1_3_2_1_34_1","volume-title":"ECOOP","author":"Zaeem R. N.","year":"2010","unstructured":"R. N. Zaeem and S. Khurshid . Contract-based data structure repair using Alloy . In ECOOP 2010 . R. N. Zaeem and S. Khurshid. Contract-based data structure repair using Alloy. In ECOOP 2010."},{"key":"e_1_3_2_1_35_1","unstructured":"The HyTeK distribution can be downloaded from http:\/\/bonnie.exp.dc.uba.ar\/hytek-oopsla.tar.gz  The HyTeK distribution can be downloaded from http:\/\/bonnie.exp.dc.uba.ar\/hytek-oopsla.tar.gz"},{"key":"e_1_3_2_1_36_1","unstructured":"http:\/\/alloy.mit.edu\/  http:\/\/alloy.mit.edu\/"}],"event":{"name":"SPLASH '14: Conference on Systems, Programming, and Applications: Software for Humanity","location":"Portland Oregon USA","acronym":"SPLASH '14","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGAda ACM Special Interest Group on Ada Programming Language"]},"container-title":["Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2660193.2660232","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2660193.2660232","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:14:43Z","timestamp":1750263283000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2660193.2660232"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,10,15]]},"references-count":34,"alternative-id":["10.1145\/2660193.2660232","10.1145\/2660193"],"URL":"https:\/\/doi.org\/10.1145\/2660193.2660232","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2714064.2660232","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2014,10,15]]},"assertion":[{"value":"2014-10-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}