{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,31]],"date-time":"2024-10-31T03:03:11Z","timestamp":1730343791540,"version":"3.28.0"},"reference-count":33,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019,10]]},"DOI":"10.23919\/fmcad.2019.8894267","type":"proceedings-article","created":{"date-parts":[[2019,11,13]],"date-time":"2019-11-13T04:25:06Z","timestamp":1573619106000},"page":"212-220","source":"Crossref","is-referenced-by-count":8,"title":["Extending enumerative function synthesis via SMT-driven classification"],"prefix":"10.23919","author":[{"given":"Haniel","family":"Barbosa","sequence":"first","affiliation":[]},{"given":"Andrew","family":"Reynolds","sequence":"additional","affiliation":[]},{"given":"Daniel","family":"Larraz","sequence":"additional","affiliation":[]},{"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462174"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168907"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065045"},{"key":"ref30","first-page":"108","article-title":"Checking safety properties using induction and a sat-solver","author":"sheeran","year":"2000","journal-title":"Formal Methods In Computer-Aided Design (FMCAD) volume 1954 of Lecture Notes in Computer Science"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/3276501"},{"key":"ref11","first-page":"251","article-title":"Accelerating syntax-guided invariant synthesis","author":"fedyukovich","year":"2018","journal-title":"Tools and Algorithms for Construction and Analysis of Systems (TACAS)"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-11245-5_5"},{"key":"ref13","first-page":"69","article-title":"ICE: A robust framework for learning invariants","author":"garg","year":"2014","journal-title":"Computer Aided Verification (CAV) volume 8559 of Lecture Notes in Computer Science"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837664"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926423"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40229-1_2"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/5.97300"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_15"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192410"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94205-6_39"},{"key":"ref4","first-page":"319","article-title":"Scaling enumerative program synthesis via divide and conquer","author":"alur","year":"2017","journal-title":"Tools and Algorithms for Construction and Analysis of Systems (TACAS) volume 10205 of Lecture Notes in Computer Science"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-017-0270-2"},{"key":"ref3","article-title":"Sygus-comp 2018: Results and analysis","author":"alur","year":"2019","journal-title":"CoRR abs\/1904 07146"},{"journal-title":"Pattern Recognition and Machine Learning","year":"2006","author":"bishop","key":"ref6"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1145\/2451116.2451150"},{"key":"ref5","first-page":"825","article-title":"Satisfiability Modulo Theories","author":"barrett","year":"2009","journal-title":"Handbook of Satisfiability volume 185 of Frontiers in Artificial Intelligence and Applications chapter 26"},{"key":"ref8","first-page":"510","article-title":"The kind 2 model checker","author":"champion","year":"2016","journal-title":"Computer Aided Verification (CAV) volume 9780 of Lecture Notes in Computer Science"},{"key":"ref7","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","article-title":"Sat-based model checking without unrolling","author":"bradley","year":"2011","journal-title":"Verification Model Checking and Abstract Interpretation (VMCAI)"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_10"},{"journal-title":"A Mathematical Introduction to Logic","year":"2001","author":"enderton","key":"ref9"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2018\/189"},{"key":"ref22","article-title":"Data-driven loop invariant inference with automatic feature synthesis","author":"padhi","year":"2017","journal-title":"CoRR abs\/1707 02029"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1145\/3173545"},{"key":"ref24","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1007\/BF00116251","article-title":"Induction of decision trees","volume":"1","author":"quinlan","year":"1986","journal-title":"Mach Learn"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908099"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_12"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_5"}],"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\/08894267.pdf?arnumber=8894267","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,23]],"date-time":"2020-08-23T18:45:37Z","timestamp":1598208337000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8894267\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10]]},"references-count":33,"URL":"https:\/\/doi.org\/10.23919\/fmcad.2019.8894267","relation":{},"subject":[],"published":{"date-parts":[[2019,10]]}}}