{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:52:02Z","timestamp":1750308722156,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":29,"publisher":"ACM","license":[{"start":{"date-parts":[[2013,7,15]],"date-time":"2013-07-15T00:00:00Z","timestamp":1373846400000},"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":[[2013,7,15]]},"DOI":"10.1145\/2483760.2483770","type":"proceedings-article","created":{"date-parts":[[2013,7,16]],"date-time":"2013-07-16T18:06:58Z","timestamp":1373998018000},"page":"23-33","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Parallel bounded analysis in code with rich invariants by refinement of field bounds"],"prefix":"10.1145","author":[{"given":"Nicol\u00e1s","family":"Rosner","sequence":"first","affiliation":[{"name":"UBA, Argentina"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Juan","family":"Galeotti","sequence":"additional","affiliation":[{"name":"Saarland University, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Santiago","family":"Berm\u00fadez","sequence":"additional","affiliation":[{"name":"ITBA, Argentina"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guido Marucci","family":"Blas","sequence":"additional","affiliation":[{"name":"ITBA, Argentina"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Santiago Perez","family":"De Rosso","sequence":"additional","affiliation":[{"name":"ITBA, Argentina"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lucas","family":"Pizzagalli","sequence":"additional","affiliation":[{"name":"ITBA, Argentina"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luciano","family":"Zem\u00edn","sequence":"additional","affiliation":[{"name":"ITBA, Argentina"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marcelo F.","family":"Frias","sequence":"additional","affiliation":[{"name":"ITBA, Argentina"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2013,7,15]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Abad P. Aguirre N. Bengolea V. Ciolek D. Frias M.F. Galeotti J. Maibaum T. Moscato M. Rosner N. Vissani I. Tight Bounds + Incremental SAT = Better Test Generation under Rich Contracts to appear in Proceedings of ICST 2013.  Abad P. Aguirre N. Bengolea V. Ciolek D. Frias M.F. Galeotti J. Maibaum T. Moscato M. Rosner N. Vissani I. Tight Bounds + Incremental SAT = Better Test Generation under Rich Contracts to appear in Proceedings of ICST 2013."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1595696.1595762"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1287624.1287653"},{"key":"e_1_3_2_1_4_1","first-page":"88","volume-title":"Using First-Order Theorem Provers in the Jahob Data Structure Verification System. VMCAI","author":"Bouillaguet Ch","year":"2007"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/566172.566191"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_16"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Cuervo-Parrino B. Galeotti J.P. Garbervetsky D. Frias M.F. A dataflow analysis to improve SAT-based program verification to appear in Proceedings of SEFM 2011.   Cuervo-Parrino B. Galeotti J.P. Garbervetsky D. Frias M.F. A dataflow analysis to improve SAT-based program verification to appear in Proceedings of SEFM 2011.","DOI":"10.1007\/978-3-642-24690-6_11"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2007.43"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146238.1146251"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1831708.1831712"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"crossref","unstructured":"Juan P. Galeotti Nicol\u00e1s Rosner Carlos L\u00f3pez Pombo Marcelo F. Frias: TACO: E\ufb03cient SAT-Based Bounded Verification Using Symmetry Breaking and Tight Bounds submitted to IEEE TSE 2013.  Juan P. Galeotti Nicol\u00e1s Rosner Carlos L\u00f3pez Pombo Marcelo F. Frias: TACO: E\ufb03cient SAT-Based Bounded Verification Using Symmetry Breaking and Tight Bounds submitted to IEEE TSE 2013.","DOI":"10.1109\/TSE.2013.15"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.3233\/SAT190063"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/337180.337616"},{"key":"e_1_3_2_1_16_1","unstructured":"Jackson D. Software Abstractions. MIT Press 2006.  Jackson D. Software Abstractions. MIT Press 2006."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/347324.383378"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:AUSE.0000038938.10589.b9"},{"key":"e_1_3_2_1_19_1","unstructured":"Leino K.R.M. Specification and verification of Object-Oriented Software Lecture Notes from Marktoberdorf International Summer School 2008.  Leino K.R.M. Specification and verification of Object-Oriented Software Lecture Notes from Marktoberdorf International Summer School 2008."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02777-2_47"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISSRE.2010.27"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_48"},{"volume-title":"FASE 2011:  262-277","author":"Rohan Sharma","key":"e_1_3_2_1_23_1"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2009.48"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1831708.1831732"},{"key":"e_1_3_2_1_26_1","first-page":"632","volume":"4425","author":"Torlak E.","journal-title":"LNCS"},{"key":"e_1_3_2_1_27_1","first-page":"505","volume-title":"TACAS","author":"Vaziri M.","year":"2003"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022920129859"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146238.1146243"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.1996.0030"}],"event":{"name":"ISSTA '13: Iitsnternational Symposium on Software Testing and Analysis","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Lugano Switzerland","acronym":"ISSTA '13"},"container-title":["Proceedings of the 2013 International Symposium on Software Testing and Analysis"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2483760.2483770","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2483760.2483770","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:14:37Z","timestamp":1750277677000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2483760.2483770"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,7,15]]},"references-count":29,"alternative-id":["10.1145\/2483760.2483770","10.1145\/2483760"],"URL":"https:\/\/doi.org\/10.1145\/2483760.2483770","relation":{},"subject":[],"published":{"date-parts":[[2013,7,15]]},"assertion":[{"value":"2013-07-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}