{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T20:13:03Z","timestamp":1784232783094,"version":"3.55.0"},"publisher-location":"New York, NY, USA","reference-count":38,"publisher":"ACM","license":[{"start":{"date-parts":[[2013,10,29]],"date-time":"2013-10-29T00:00:00Z","timestamp":1383004800000},"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,10,29]]},"DOI":"10.1145\/2509578.2509586","type":"proceedings-article","created":{"date-parts":[[2013,10,23]],"date-time":"2013-10-23T15:29:17Z","timestamp":1382542157000},"page":"135-152","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":157,"title":["Growing solver-aided languages with rosette"],"prefix":"10.1145","author":[{"given":"Emina","family":"Torlak","sequence":"first","affiliation":[{"name":"University of California Berkeley, Berkeley, CA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rastislav","family":"Bodik","sequence":"additional","affiliation":[{"name":"University of California Berkeley, Berkeley, CA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2013,10,29]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/2023474.2023512"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/646484.691763"},{"key":"e_1_3_2_1_3_1","unstructured":"AIGER. fmv.jku.at\/aiger\/.  AIGER. fmv.jku.at\/aiger\/."},{"key":"e_1_3_2_1_4_1","volume-title":"AR Meetings. www.ar.al-anon.alateen.org\/alanonmeetings.htm.","author":"Al-Anon","unstructured":"Al-Anon AR Meetings. www.ar.al-anon.alateen.org\/alanonmeetings.htm. Al-Anon AR Meetings. www.ar.al-anon.alateen.org\/alanonmeetings.htm."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"e_1_3_2_1_6_1","unstructured":"Berkeley Logic Synthesis and Verification Group. ABC: A system for sequential synthesis and verification. www.eecs.berkeley.edu\/~alanmi\/abc\/.  Berkeley Logic Synthesis and Verification Group. ABC: A system for sequential synthesis and verification. www.eecs.berkeley.edu\/~alanmi\/abc\/."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985811"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_15"},{"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\/1146238.1146251"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1287624.1287653"},{"key":"e_1_3_2_1_14_1","volume-title":"Semantics Engineering with PLT Redex","author":"Felleisen M.","year":"2009","unstructured":"M. Felleisen , R. B. Findler , and M. Flatt . Semantics Engineering with PLT Redex . The MIT Press , 1 st edition, 2009 . ISBN 0262062755, 9780262062756. M. Felleisen, R. B. Findler, and M. Flatt. Semantics Engineering with PLT Redex. The MIT Press, 1st edition, 2009. ISBN 0262062755, 9780262062756.","edition":"1"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1831708.1831712"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993506"},{"key":"e_1_3_2_1_18_1","unstructured":"IMDb Top 250 movies. www.imdb.com\/chart\/top.  IMDb Top 250 movies. www.imdb.com\/chart\/top."},{"key":"e_1_3_2_1_19_1","unstructured":"iTunes Top 100 Songs. www.apple.com\/itunes\/charts\/songs\/.  iTunes Top 100 Songs. www.apple.com\/itunes\/charts\/songs\/."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/11527695_15"},{"key":"e_1_3_2_1_21_1","unstructured":"JavaPathFinder. babelfish.arc.nasa.gov\/trac\/jpf\/.  JavaPathFinder. babelfish.arc.nasa.gov\/trac\/jpf\/."},{"key":"e_1_3_2_1_22_1","volume-title":"Computer Aided Verification (CAV) verification","author":"Jose M.","year":"2011","unstructured":"M. Jose and R. Majumdar . Bug-Assist: assisting fault localization in ansi-c programs . In Computer Aided Verification (CAV) verification , 2011 . M. Jose and R. Majumdar. Bug-Assist: assisting fault localization in ansi-c programs. In Computer Aided Verification (CAV) verification, 2011."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103675"},{"key":"e_1_3_2_1_24_1","volume-title":"Logic for Programming, Artificial Intelligence","author":"Leino K. R. M.","year":"2010","unstructured":"K. R. M. Leino . Dafny : an automatic program verifier for functional correctness . In Logic for Programming, Artificial Intelligence , and Reasoning (LPAR) , 2010 . K. R. M. Leino. Dafny: an automatic program verifier for functional correctness. In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), 2010."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_26"},{"key":"e_1_3_2_1_26_1","volume-title":"Executable specifications for Java programs. Master's thesis","author":"Milicevic A.","year":"2010","unstructured":"A. Milicevic . Executable specifications for Java programs. Master's thesis , Massachusetts Institute of Technology , 2010 . A. Milicevic. Executable specifications for Java programs. Master's thesis, Massachusetts Institute of Technology, 2010."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2393596.2393667"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/1883978.1884016"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_2"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1039991.1039992"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2076674.2076677"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/1883978.1884015"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/2075089.2075119"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168907"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/2041552.2041575"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706345"},{"key":"e_1_3_2_1_39_1","unstructured":"The Racket Programming Language. racket-lang.org.  The Racket Programming Language. racket-lang.org."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806635"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1735223.1735249"},{"key":"e_1_3_2_1_42_1","unstructured":"XPath. XML Path Language. www.w3.org\/TR\/xpath\/.  XPath. XML Path Language. www.w3.org\/TR\/xpath\/."},{"key":"e_1_3_2_1_43_1","unstructured":"D. Yoo. Fudging up Racket. hashcollision.org\/brainfudge.  D. Yoo. Fudging up Racket. hashcollision.org\/brainfudge."}],"event":{"name":"SPLASH '13: Conference on Systems, Programming, and Applications: Software for Humanity","location":"Indianapolis Indiana USA","acronym":"SPLASH '13","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 2013 ACM international symposium on New ideas, new paradigms, and reflections on programming & software"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2509578.2509586","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2509578.2509586","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:28:30Z","timestamp":1750231710000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2509578.2509586"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,10,29]]},"references-count":38,"alternative-id":["10.1145\/2509578.2509586","10.1145\/2509578"],"URL":"https:\/\/doi.org\/10.1145\/2509578.2509586","relation":{},"subject":[],"published":{"date-parts":[[2013,10,29]]},"assertion":[{"value":"2013-10-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}