{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:03:18Z","timestamp":1760043798504,"version":"3.40.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030720155"},{"type":"electronic","value":"9783030720162"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,20]],"date-time":"2021-03-20T00:00:00Z","timestamp":1616198400000},"content-version":"vor","delay-in-days":78,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Form validators based on regular expressions are often used on digital forms to prevent users from inserting data in the wrong format. However, writing these validators can pose a challenge to some users.<\/jats:p><jats:p>We present<jats:sc>Forest<\/jats:sc>, a regular expression synthesizer for digital form validations.<jats:sc>Forest<\/jats:sc>produces a regular expression that matches the desired pattern for the input values and a set of conditions over capturing groups that ensure the validity of integer values in the input. Our synthesis procedure is based on enumerative search and uses a Satisfiability Modulo Theories (SMT) solver to explore and prune the search space. We propose a novel representation for regular expressions synthesis, multi-tree, which induces patterns in the examples and uses them to split the problem through a divide-and-conquer approach. We also present a new SMT encoding to synthesize capture conditions for a given regular expression. To increase confidence in the synthesized regular expression, we implement user interaction based on distinguishing inputs.<\/jats:p><jats:p>We evaluated<jats:sc>Forest<\/jats:sc>on real-world form-validation instances using regular expressions. Experimental results show that<jats:sc>Forest<\/jats:sc>successfully returns the desired regular expression in 70% of the instances and outperforms<jats:sc>Regel<\/jats:sc>, a state-of-the-art regular expression synthesizer.<\/jats:p>","DOI":"10.1007\/978-3-030-72016-2_9","type":"book-chapter","created":{"date-parts":[[2021,3,19]],"date-time":"2021-03-19T22:03:37Z","timestamp":1616191417000},"page":"152-169","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["FOREST: An Interactive Multi-tree Synthesizer for Regular Expressions"],"prefix":"10.1007","author":[{"given":"Margarida","family":"Ferreira","sequence":"first","affiliation":[]},{"given":"Miguel","family":"Terra-Neves","sequence":"additional","affiliation":[]},{"given":"Miguel","family":"Ventura","sequence":"additional","affiliation":[]},{"given":"In\u00eas","family":"Lynce","sequence":"additional","affiliation":[]},{"given":"Ruben","family":"Martins","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,3,20]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Chen, Q., Wang, X., Ye, X., Durrett, G., Dillig, I.: Multi-modal synthesis of regular expressions. In: PLDI. ACM (2020)","DOI":"10.1145\/3385412.3385988"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"Chen, Y., Martins, R., Feng, Y.: Maximal multi-layer specification synthesis. In: ESEC\/SIGSOFT FSE. pp. 602\u2013612. ACM (2019)","DOI":"10.1145\/3338906.3338951"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Fedyukovich, G., Gupta, A.: Functional synthesis with examples. In: CP. Lecture Notes in Computer Science, vol. 11802, pp. 547\u2013564. Springer (2019)","DOI":"10.1007\/978-3-030-30048-7_32"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Feng, Y., Martins, R., Bastani, O., Dillig, I.: Program synthesis using conflict-driven learning. In: PLDI. pp. 420\u2013435. ACM (2018)","DOI":"10.1145\/3296979.3192382"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Feng, Y., Martins, R., Geffen, J.V., Dillig, I., Chaudhuri, S.: Component-based synthesis of table consolidation and transformation tasks from examples. In: PLDI. pp. 422\u2013436. ACM (2017)","DOI":"10.1145\/3140587.3062351"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Golia, P., Roy, S., Meel, K.S.: Manthan: A data driven approach for boolean function synthesis. In: CAV. Springer (2020)","DOI":"10.1007\/978-3-030-53291-8_31"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Gulwani, S.: Automating string processing in spreadsheets using input-output examples. In: POPL. pp. 317\u2013330. ACM (2011)","DOI":"10.1145\/1925844.1926423"},{"key":"9_CR8","unstructured":"Kini, D., Gulwani, S.: Flashnormalize: Programming by examples for text normalization. In: IJCAI. pp. 776\u2013783. AAAI Press (2015)"},{"key":"9_CR9","unstructured":"Kushman, N., Barzilay, R.: Using semantic unification to generate regular expressions from natural language. In: HLT-NAACL. pp. 826\u2013836. The Association for Computational Linguistics (2013)"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Lee, M., So, S., Oh, H.: Synthesizing regular expressions from examples for introductory automata assignments. In: GPCE. pp. 70\u201380. ACM (2016)","DOI":"10.1145\/3093335.2993244"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"Li, H., Chan, C., Maier, D.: Query from examples: An iterative, data-driven approach to query construction. Proc. VLDB Endow. 8(13), 2158\u20132169 (2015)","DOI":"10.14778\/2831360.2831369"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Locascio, N., Narasimhan, K., DeLeon, E., Kushman, N., Barzilay, R.: Neural generation of regular expressions from natural language with minimal domain knowledge. In: EMNLP. pp. 1918\u20131923. The Association for Computational Linguistics (2016)","DOI":"10.18653\/v1\/D16-1197"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Martins, R., Chen, J., Chen, Y., Feng, Y., Dillig, I.: Trinity: An Extensible Synthesis Framework for Data Science. PVLDB 12(12), 1914\u20131917 (2019)","DOI":"10.14778\/3352063.3352098"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Mayer, M., Soares, G., Grechkin, M., Le, V., Marron, M., Polozov, O., Singh,R., Zorn, B.G., Gulwani, S.: User interaction models for disambiguation in programming by example. In: UIST. pp. 291\u2013301. ACM (2015)","DOI":"10.1145\/2807442.2807459"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: TACAS. Lecture Notes in Computer Science, vol.\u00a04963, pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9_CR16","unstructured":"Orvalho, P., Terra-Neves, M., Ventura, M., Martins, R., Manquinho, V.M.:Squares. https:\/\/squares-sql.github.io, accessed on May 27, 2020"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"Orvalho, P., Terra-Neves, M., Ventura, M., Martins, R., Manquinho, V.M.: Encodings for enumeration-based program synthesis. In: CP. Lecture Notes in Computer Science, vol. 11802, pp. 583\u2013599. Springer (2019)","DOI":"10.1007\/978-3-030-30048-7_34"},{"key":"9_CR18","unstructured":"Python Software Foundation: Python3\u2019s regular expression module re. https:\/\/docs.python.org\/3\/library\/re.html, accessed on October 11, 2020"},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Raza, M., Gulwani, S.: Automated data extraction using predictive program synthesis. In: AAAI. pp. 882\u2013890. AAAI Press (2017)","DOI":"10.1609\/aaai.v31i1.10668"},{"key":"9_CR20","unstructured":"Regular Expression Library: www.regexlib.com, accessed on May 27, 2020"},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Barbosa, H., N\u00f6tzli, A., Barrett, C.W., Tinelli, C.: cvc4sy: Smart and fast term enumeration for syntax-guided synthesis. In: CAV. Lecture Notes in Computer Science, vol. 11562, pp. 74\u201383. Springer(2019)","DOI":"10.1007\/978-3-030-25543-5_5"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A.: Program sketching. Int. J. Softw. Tools Technol. Transf. 15(5-6), 475\u2013495 (2013)","DOI":"10.1007\/s10009-012-0249-7"},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"Stanford, C., Veanes, M., Bj\u00f8rner, N.: Symbolic boolean derivatives for efficiently solving extended regular expression constraints. Tech. Rep. MSR-TR-2020-25, Microsoft (August 2020), updated November 2020.","DOI":"10.1145\/3410296"},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"Wang, C., Cheung, A., Bod\u00edk, R.: Interactive query synthesis from input-output examples. In: SIGMOD Conference. pp. 1631\u20131634. ACM (2017)","DOI":"10.1145\/3035918.3058738"},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"Wang, C., Cheung, A., Bod\u00edk, R.: Synthesizing highly expressive SQL queries from input-output examples. In: PLDI. pp. 452\u2013466. ACM (2017)","DOI":"10.1145\/3140587.3062365"},{"key":"9_CR26","doi-asserted-by":"crossref","unstructured":"Wang, X., Gulwani, S., Singh, R.: FIDEX: filtering spreadsheet data using examples. In: OOPSLA. pp. 195\u2013213. ACM (2016)","DOI":"10.1145\/3022671.2984030"},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"Zhong, Z., Guo, J., Yang, W., Peng, J., Xie, T., Lou, J., Liu, T., Zhang, D.: Semregex: A semantics-based approach for generating regular expressions from natural language specifications. In: EMNLP. pp. 1608\u20131618. Association for Computational Linguistics (2018)","DOI":"10.18653\/v1\/D18-1189"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-72016-2_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,22]],"date-time":"2022-12-22T01:01:11Z","timestamp":1671670871000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-72016-2_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720155","9783030720162"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72016-2_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"20 March 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/tacas","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":"141","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":"41","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":"21","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":"29% - 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":"12","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)"}},{"value":"The conference changed to an online format due to the COVID-19 pandemic","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}