{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,31]],"date-time":"2024-10-31T03:03:07Z","timestamp":1730343787679,"version":"3.28.0"},"reference-count":27,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019,10]]},"DOI":"10.23919\/fmcad.2019.8894251","type":"proceedings-article","created":{"date-parts":[[2019,11,13]],"date-time":"2019-11-13T09:25:06Z","timestamp":1573637106000},"page":"203-211","source":"Crossref","is-referenced-by-count":4,"title":["GUIDEDSAMPLER: Coverage-guided Sampling of SMT Solutions"],"prefix":"10.23919","author":[{"given":"Rafael","family":"Dutra","sequence":"first","affiliation":[]},{"given":"Jonathan","family":"Bachrach","sequence":"additional","affiliation":[]},{"given":"Koushik","family":"Sen","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_11"},{"journal-title":"The Satisfiability Modulo Theories Library (SMT-LIB)","year":"2016","author":"barrett","key":"ref11"},{"key":"ref12","article-title":"Uniform solution sampling using a constraint solver as an oracle","author":"ermon","year":"2012","journal-title":"Conference on Uncertainty in Artificial Intelligence"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_25"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/3240765.3240848"},{"journal-title":"Sampling techniques for boolean satisfiability","year":"2014","author":"meel","key":"ref15"},{"key":"ref16","first-page":"670","article-title":"Towards efficient sampling: Exploiting random walk strategies","volume":"4","author":"wei","year":"2004","journal-title":"AAAI"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2007.4397275"},{"journal-title":"Markov chain Monte Carlo stimulus generation for constrained random simulation","year":"2010","author":"kitchen","key":"ref18"},{"key":"ref19","first-page":"287","article-title":"Generating diverse solutions in sat","author":"nadel","year":"2011","journal-title":"SAT"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/CSCWD.2009.4968035"},{"key":"ref27","first-page":"194","article-title":"?z-an optimizing smt solver","volume":"15","author":"bj\u00f8rner","year":"2015","journal-title":"TACAS"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1145\/1168918.1168907"},{"key":"ref6","article-title":"Ivy: interactive verification of parameterized systems via effectively propositional reasoning","author":"padon","year":"2016","journal-title":"PLDI ACM"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40627-0_60"},{"key":"ref8","article-title":"CUTE: A concolic unit testing engine for C","author":"sen","year":"2005","journal-title":"ESEClFSE’05"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180248"},{"key":"ref9","article-title":"KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs","author":"cadar","year":"2008","journal-title":"OSDI’08"},{"key":"ref1","first-page":"13","article-title":"Constraint-based random stimuli generation for hardware verification","volume":"28","author":"naveh","year":"2007","journal-title":"AI Magazine"},{"key":"ref20","first-page":"2085","article-title":"Embed and project: Discrete sampling with universal hashing","author":"ermon","year":"2013","journal-title":"Advances in neural information processing systems"},{"key":"ref22","first-page":"1","article-title":"Balancing scalability and uniformity in sat witness generator","author":"chakraborty","year":"2014","journal-title":"2014 51st ACM\/EDAC\/IEEE Design Automation Conference (DAC) DAC"},{"key":"ref21","article-title":"Constrained sampling and counting: Universal hashing meets sat solving","author":"meel","year":"2016","journal-title":"Beyond NP AAAI Workshops"},{"key":"ref24","article-title":"Waps: Weighted and projected sampling","author":"gupta","year":"2019","journal-title":"Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS)"},{"key":"ref23","article-title":"Distribution-aware sampling and weighted model counting for SAT","volume":"7","author":"chakraborty","year":"2014","journal-title":"Proceedings of AAAI Conference on Artificial Intelligence (AAAI)"},{"key":"ref26","first-page":"337","article-title":"Z3: An efficient smt solver","author":"de moura","year":"2008","journal-title":"Tools and Algorithms for the Construction and Analysis of Systems"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/11814948_18"}],"event":{"name":"2019 Formal Methods in Computer Aided Design (FMCAD)","start":{"date-parts":[[2019,10,22]]},"location":"San Jose, CA, USA","end":{"date-parts":[[2019,10,25]]}},"container-title":["2019 Formal Methods in Computer Aided Design (FMCAD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8891869\/8894241\/08894251.pdf?arnumber=8894251","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,23]],"date-time":"2020-08-23T22:45:12Z","timestamp":1598222712000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8894251\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10]]},"references-count":27,"URL":"https:\/\/doi.org\/10.23919\/fmcad.2019.8894251","relation":{},"subject":[],"published":{"date-parts":[[2019,10]]}}}