{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T06:02:00Z","timestamp":1726034520747},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030242572"},{"type":"electronic","value":"9783030242589"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-24258-9_20","type":"book-chapter","created":{"date-parts":[[2019,6,28]],"date-time":"2019-06-28T21:02:31Z","timestamp":1561755751000},"page":"279-297","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Syntax-Guided Rewrite Rule Enumeration for SMT Solvers"],"prefix":"10.1007","author":[{"ORCID":"http:\/\/orcid.org\/0000-0001-8669-0011","authenticated-orcid":false,"given":"Andres","family":"N\u00f6tzli","sequence":"first","affiliation":[]},{"ORCID":"http:\/\/orcid.org\/0000-0002-3529-8682","authenticated-orcid":false,"given":"Andrew","family":"Reynolds","sequence":"additional","affiliation":[]},{"ORCID":"http:\/\/orcid.org\/0000-0003-0188-2300","authenticated-orcid":false,"given":"Haniel","family":"Barbosa","sequence":"additional","affiliation":[]},{"ORCID":"http:\/\/orcid.org\/0000-0003-2600-5283","authenticated-orcid":false,"given":"Aina","family":"Niemetz","sequence":"additional","affiliation":[]},{"ORCID":"http:\/\/orcid.org\/0000-0002-7142-6258","authenticated-orcid":false,"given":"Mathias","family":"Preiner","sequence":"additional","affiliation":[]},{"ORCID":"http:\/\/orcid.org\/0000-0002-9522-3084","authenticated-orcid":false,"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[]},{"ORCID":"http:\/\/orcid.org\/0000-0002-6726-775X","authenticated-orcid":false,"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,6,29]]},"reference":[{"key":"20_CR1","unstructured":"SMT-COMP 2018 (2018) http:\/\/smtcomp.sourceforge.net\/2018\/"},{"key":"20_CR2","unstructured":"SyGuS-COMP 2018 (2018). http:\/\/sygus.seas.upenn.edu\/SyGuS-COMP2018.html"},{"key":"20_CR3","unstructured":"CVC4 sat2019 branch (2019). https:\/\/github.com\/4tXJ7f\/CVC4\/tree\/sat2019"},{"key":"20_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/978-3-319-96145-3_15","volume-title":"Computer Aided Verification","author":"A Abate","year":"2018","unstructured":"Abate, A., David, C., Kesseli, P., Kroening, D., Polgreen, E.: Counterexample guided inductive synthesis modulo theories. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 270\u2013288. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_15"},{"key":"20_CR5","unstructured":"Akiba, T., et al.: Calibrating research in program synthesis using 72,000 hours of programmer time. Technical Report, MSR, Redmond, WA, USA (2013)"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"Alur, R., et al.: Syntax-guided synthesis. In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, 20\u201323 October 2013. pp. 1\u20138. IEEE (2013) http:\/\/ieeexplore.ieee.org\/document\/6679385\/","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"20_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-662-54577-5_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Alur","year":"2017","unstructured":"Alur, R., Radhakrishna, A., Udupa, A.: Scaling enumerative program synthesis via divide and conquer. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 319\u2013336. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_18"},{"key":"20_CR8","doi-asserted-by":"publisher","unstructured":"Bansal, S., Aiken, A.: Automatic generation of peephole superoptimizers. In: Shen, J.P., Martonosi, M. (eds.) Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2006, San Jose, CA, USA, 21\u201325 October 2006. pp. 394\u2013403. ACM (2006), https:\/\/doi.org\/10.1145\/1168857.1168906","DOI":"10.1145\/1168857.1168906"},{"key":"20_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14"},{"key":"20_CR10","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2016). www.SMT-LIB.org"},{"key":"20_CR11","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.6. Technical report, Department of Computer Science, The University of Iowa (2017). www.SMT-LIB.org"},{"key":"20_CR12","doi-asserted-by":"publisher","unstructured":"Berzish, M., Ganesh, V., Zheng, Y.: Z3str3: A string solver with theory-aware heuristics. In: 2017 Formal Methods in Computer Aided Design, FMCAD 2017, Vienna, Austria, 2\u20136 October 2017. pp. 55\u201359 (2017). https:\/\/doi.org\/10.23919\/FMCAD.2017.8102241","DOI":"10.23919\/FMCAD.2017.8102241"},{"key":"20_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/978-3-319-96142-2_6","volume-title":"Computer Aided Verification","author":"D Blotsky","year":"2018","unstructured":"Blotsky, D., Mora, F., Berzish, M., Zheng, Y., Kabir, I., Ganesh, V.: StringFuzz: a fuzzer for string solvers. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 45\u201351. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_6"},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"Brummayer, R., Biere, A.: Fuzzing and delta-debugging SMT solvers. In: Proceedings of the 7th International Workshop on Satisfiability Modulo Theories, SMT 2009, p. 5. ACM (2009)","DOI":"10.1145\/1670412.1670413"},{"key":"20_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-662-46663-6_9","volume-title":"Compiler Construction","author":"S Buchwald","year":"2015","unstructured":"Buchwald, S.: Optgen: a generator for local optimizations. In: Franke, B. (ed.) CC 2015. LNCS, vol. 9031, pp. 171\u2013189. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46663-6_9"},{"key":"20_CR16","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Draves, R., van Renesse, R. (eds.) Proceedings of 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, 8\u201310 December 2008, San Diego, California, USA, pp. 209\u2013224. USENIX Association (2008). http:\/\/www.usenix.org\/events\/osdi08\/tech\/full_papers\/cadar\/cadar.pdf"},{"key":"20_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-642-39611-3_21","volume-title":"Hardware and Software: Verification and Testing","author":"V Ganesh","year":"2013","unstructured":"Ganesh, V., Minnes, M., Solar-Lezama, A., Rinard, M.: Word equations with length constraints: what\u2019s decidable? In: Biere, A., Nahir, A., Vos, T. (eds.) HVC 2012. LNCS, vol. 7857, pp. 209\u2013226. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39611-3_21"},{"key":"20_CR18","unstructured":"Hansen, T.: A constraint solver and its application to machine code test generation. Ph.D. thesis, University of Melbourne, Australia (2012). http:\/\/hdl.handle.net\/11343\/37952"},{"key":"20_CR19","volume-title":"Hacker\u2019s Delight","author":"HS Warren Jr","year":"2013","unstructured":"Warren Jr., H.S.: Hacker\u2019s Delight, 2nd edn. Pearson Education, London (2013). http:\/\/www.hackersdelight.org\/","edition":"2"},{"key":"20_CR20","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Leonardo de Moura","year":"2008","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, pp. 337\u2013340 (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"20_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"663","DOI":"10.1007\/978-3-319-08867-9_44","volume-title":"Computer Aided Verification","author":"A Nadel","year":"2014","unstructured":"Nadel, A.: Bit-vector rewriting with automatic rule generation. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 663\u2013679. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_44"},{"key":"20_CR22","doi-asserted-by":"crossref","unstructured":"Niemetz, A., Preiner, M., Biere, A.: Boolector 2.0 system description. J. Satis. Boolean Model. Comput. 9, 53\u201358 (2014, published 2015)","DOI":"10.3233\/SAT190101"},{"key":"20_CR23","unstructured":"Niemetz, A., Preiner, M., Biere, A.: Model-Based API Testing for SMT Solvers. In: Brain, M., Hadarean, L. (eds.) Proceedings of the 15th International Workshop on Satisfiability Modulo Theories, SMT 2017), affiliated with the 29th International Conference on Computer Aided Verification, CAV 2017, Heidelberg, Germany, 24\u201328 July 2017, p. 10 (2017)"},{"key":"20_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/978-3-319-96142-2_16","volume-title":"Computer Aided Verification","author":"A Niemetz","year":"2018","unstructured":"Niemetz, A., Preiner, M., Reynolds, A., Barrett, C., Tinelli, C.: Solving quantified bit-vectors using invertibility conditions. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 236\u2013255. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_16"},{"key":"20_CR25","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Barbosa, H., N\u00f6tzil, A., Barrett, C., Tinelli, C.: CVC4Sy: Smart and fast term enumeration for syntax-guided synthesis. In: Dilig, I., Tasiran, S. (eds.) Computer Aided Verification (CAV) - 31st International Conference. Lecture Notes in Computer Science, Springer (2019, Accepted for publication)","DOI":"10.1007\/978-3-030-25543-5_5"},{"key":"20_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/978-3-319-21668-3_12","volume-title":"Computer Aided Verification","author":"A Reynolds","year":"2015","unstructured":"Reynolds, A., Deters, M., Kuncak, V., Tinelli, C., Barrett, C.: Counterexample-guided quantifier instantiation for synthesis in SMT. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 198\u2013216. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21668-3_12"},{"key":"20_CR27","doi-asserted-by":"publisher","first-page":"81","DOI":"10.4204\/EPTCS.260.8","volume":"260","author":"Andrew Reynolds","year":"2017","unstructured":"Reynolds, A., Tinelli, C.: SyGuS techniques in the core of an SMT solver. In: Proceedings Sixth Workshop on Synthesis, SYNT@CAV 2017, Heidelberg, Germany, 22nd July 2017, pp. 81\u201396 (2017). https:\/\/doi.org\/10.4204\/EPTCS.260.8","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"20_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/978-3-319-63390-9_24","volume-title":"Computer Aided Verification","author":"A Reynolds","year":"2017","unstructured":"Reynolds, A., Woo, M., Barrett, C., Brumley, D., Liang, T., Tinelli, C.: Scaling Up DPLL(T) string solvers using context-dependent simplification. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 453\u2013474. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_24"},{"key":"20_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/978-3-642-39176-7_19","volume-title":"Model Checking Software","author":"A Romano","year":"2013","unstructured":"Romano, A., Engler, D.: Expression reduction from programs in a symbolic binary executor. In: Bartocci, E., Ramakrishnan, C.R. (eds.) SPIN 2013. LNCS, vol. 7976, pp. 301\u2013319. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39176-7_19"},{"key":"20_CR30","doi-asserted-by":"publisher","unstructured":"Schkufza, E., Sharma, R., Aiken, A.: Stochastic superoptimization. In: Sarkar, V., Bod\u00edk, R. (eds.) Architectural Support for Programming Languages and Operating Systems, ASPLOS 2013, Houston, TX, USA - 16\u201320 March 2013, pp. 305\u2013316. ACM (2013). https:\/\/doi.org\/10.1145\/2451116.2451150","DOI":"10.1145\/2451116.2451150"},{"key":"20_CR31","doi-asserted-by":"publisher","unstructured":"Singh, R., Solar-Lezama, A.: SWAPPER: A framework for automatic generation of formula simplifiers based on conditional rewrite rules. In: Piskac, R., Talupur, M. (eds.) 2016 Formal Methods in Computer-Aided Design, FMCAD 2016, Mountain View, CA, USA, 3\u20136 October 2016, pp. 185\u2013192. IEEE (2016). https:\/\/doi.org\/10.1109\/FMCAD.2016.7886678","DOI":"10.1109\/FMCAD.2016.7886678"},{"key":"20_CR32","unstructured":"Tinelli, C., Barrett, C., Fontaine, P.: Unicode Strings (Draft 1.0) (2018). http:\/\/smtlib.cs.uiowa.edu\/theories-UnicodeStrings.shtml"},{"key":"20_CR33","doi-asserted-by":"publisher","unstructured":"Udupa, A., Raghavan, A., Deshmukh, J.V., Mador-Haim, S., Martin, M.M.K., Alur, R.: TRANSIT: specifying protocols with concolic snippets. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2013, Seattle, WA, USA, 16\u201319 June 2013, pp. 287\u2013296 (2013). https:\/\/doi.org\/10.1145\/2462156.2462174","DOI":"10.1145\/2462156.2462174"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2019"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-24258-9_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,22]],"date-time":"2022-09-22T10:32:43Z","timestamp":1663842763000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-24258-9_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030242572","9783030242589"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-24258-9_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"29 June 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAT","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Theory and Applications of Satisfiability Testing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 July 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sat2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/sat2019.tecnico.ulisboa.pt\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"64","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"19","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"7","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}