{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:27:38Z","timestamp":1750220858838,"version":"3.41.0"},"reference-count":26,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2019,12,2]],"date-time":"2019-12-02T00:00:00Z","timestamp":1575244800000},"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":["SIGSOFT Softw. Eng. Notes"],"published-print":{"date-parts":[[2019,12,2]]},"abstract":"<jats:p>Tools that explore very large state spaces to nd bugs, e.g., when model checking, or to nd solutions, e.g., when constraint solving, can take a considerable amount of time before the search termi- nates, and the user may not get useful feedback on the state of the search during that time. Our focus is a tool that solves im- perative constraints to provide automated test input generation for systematic testing. Speci cally, we introduce a technique to quantify the exploration of Korat, a well-known tool that explores the bounded space of all candidate inputs and enumerates desired inputs that satisfy given constraints. Our technique quanti es the size of the input space as it is explored by the Korat search, and provides the user exact information on the size of the remaining input space. In addition, it allows studying key characteristics of the search, such as the distribution of solutions as the search nds them. We implement the technique as a listener for the Korat search, and present initial experimental results using it.<\/jats:p>","DOI":"10.1145\/3364452.3364456","type":"journal-article","created":{"date-parts":[[2019,12,13]],"date-time":"2019-12-13T14:08:57Z","timestamp":1576246137000},"page":"15-19","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Quantifying the Exploration of the Korat Solver for Imperative Constraints"],"prefix":"10.1145","volume":"44","author":[{"given":"Alyas","family":"Almaawi","sequence":"first","affiliation":[{"name":"University of Texas at Austin, Austin, TX, USA"}]},{"given":"Hayes","family":"Converse","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, Austin, TX, USA"}]},{"given":"Milos","family":"Gligoric","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, Austin, TX, USA"}]},{"given":"Sasa","family":"Misailovic","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Urbana, IL, USA"}]},{"given":"Sarfraz","family":"Khurshid","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, Austin, TX, USA"}]}],"member":"320","published-online":{"date-parts":[[2019,12,12]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Korat GitHub repository 2019. https:\/\/github.com\/korattest\/korat."},{"key":"e_1_2_1_2_1","volume-title":"A study of the solution distributions for structural constraints using Korat. Under submission","author":"Almaawi A.","year":"2019","unstructured":"A. Almaawi, N. Dini, C. Yelen, M. Gligoric, S. Misailovic, and S. Khurshid. A study of the solution distributions for structural constraints using Korat. Under submission, 2019."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/513918.514103"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/869107"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/566172.566191"},{"key":"e_1_2_1_6_1","volume-title":"OSDI","author":"Cadar C.","year":"2008","unstructured":"C. Cadar, D. Dunbar, and D. R. Engler. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In OSDI, 2008."},{"key":"e_1_2_1_7_1","volume-title":"Model Checking","author":"Clarke E. M.","year":"1999","unstructured":"E. M. Clarke, Jr., O. Grumberg, and D. A. Peled. Model Checking. MIT Press, Cambridge, MA, USA, 1999."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_1_9_1","volume-title":"SAT","author":"Een N.","year":"2003","unstructured":"N. Een and N. Sorensson. An extensible SAT-solver. In SAT, 2003."},{"key":"e_1_2_1_10_1","first-page":"1","volume":"13","author":"Felgentre T.","year":"2014","unstructured":"T. Felgentre , A. Borning, and R. Hirschfeld. Specifying and solving constraints on object behavior. The Journal of Object Technology, 13:1:1, 04 2014.","journal-title":"Specifying and solving constraints on object behavior. The Journal of Object Technology"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_2_1_12_1","first-page":"24","volume-title":"INAP","author":"Hofstedt P.","year":"2005","unstructured":"P. Hofstedt and O. Krzikalla. TURTLE++ { a CIP-library for C++. In INAP, pages 12{24, 2005."},{"key":"e_1_2_1_13_1","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"Jackson D.","year":"2012","unstructured":"D. Jackson. Software Abstractions: Logic, Language, and Analysis. The MIT Press, 2012."},{"key":"e_1_2_1_14_1","volume-title":"AAAI","author":"Kilby P.","year":"2006","unstructured":"P. Kilby, J. K. Slaney, S. Thi--ebaux, and T. Walsh. Estimating search tree size. In AAAI, 2006."},{"key":"e_1_2_1_15_1","volume-title":"Symbolic execution and program testing. CACM, 19(7)","author":"King J. C.","year":"1976","unstructured":"J. C. King. Symbolic execution and program testing. CACM, 19(7), 1976."},{"key":"e_1_2_1_16_1","volume-title":"Estimating the efficiency of backtrack programs. Mathematics of Computation, 29(129)","author":"Knuth D.","year":"1975","unstructured":"D. Knuth. Estimating the efficiency of backtrack programs. Mathematics of Computation, 29(129), 1975."},{"key":"e_1_2_1_17_1","volume-title":"Progress bar for SAT solvers. Unpublished manuscript","author":"Kokotov D.","year":"2000","unstructured":"D. Kokotov and I. Shlyakhter. Progress bar for SAT solvers. Unpublished manuscript, 2000."},{"key":"e_1_2_1_18_1","volume-title":"Speci cation, and Object-Oriented Design.","author":"Liskov B.","year":"2000","unstructured":"B. Liskov and J. Guttag. Program Development in Java: Abstraction, Speci cation, and Object-Oriented Design. 2000."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/872023.872551"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2015.77"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1081706.1081750"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065045"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2009.24"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/786768.786967"},{"key":"e_1_2_1_26_1","volume-title":"JPF","author":"Wang K.","year":"2018","unstructured":"K. Wang, H. Converse, M. Gligoric, S. Misailovic, and S. Khurshid. A progress bar for the JPF search using program executions. In JPF, 2018."}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3364452.3364456","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3364452.3364456","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:23:29Z","timestamp":1750202609000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3364452.3364456"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,2]]},"references-count":26,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2019,12,2]]}},"alternative-id":["10.1145\/3364452.3364456"],"URL":"https:\/\/doi.org\/10.1145\/3364452.3364456","relation":{},"ISSN":["0163-5948"],"issn-type":[{"type":"print","value":"0163-5948"}],"subject":[],"published":{"date-parts":[[2019,12,2]]},"assertion":[{"value":"2019-12-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}