FOREST：一个交互式正则表达式多树合成器
FOREST: An Interactive Multi-tree Synthesizer for Regular Expressions
摘要：
基于正则表达式的表单验证器通常用于数字表单，以防止用户以错误的格式插入数据。但是，编写这些验证器可能会对某些用户构成挑战。我们提出了森林，一个正则表达式合成器的数字形式验证。FOREST生成一个正则表达式，该表达式匹配输入值所需的模式，并生成一组捕获组的条件，以确保输入中整数值的有效性。我们的合成过程是基于枚举搜索和使用可满足性模理论（SMT）求解器，探索和修剪的搜索空间。我们提出了一种新的正则表达式合成表示，多树，它诱导的例子中的模式，并使用它们来分裂的问题，通过分治的方法。我们还提出了一个新的SMT编码合成捕获条件，为一个给定的正则表达式。为了提高合成正则表达式的可信度，我们实现了基于区分输入的用户交互。我们使用正则表达式在真实世界的表单验证实例上评估了FOREST。实验结果表明，FOREST在72%的实例中成功地返回了所需的正则表达式，并优于REGEL，一个最先进的正则表达式合成器。
英文摘要：
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. We present FOREST, a regular expression synthesizer for digital form validations. FOREST 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. We evaluated FOREST on real-world form-validation instances using regular expressions. Experimental results show that FOREST successfully returns the desired regular expression in 72% of the instances and outperforms REGEL, a state-of-the-art regular expression synthesizer.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
