Synthesizing Transducers from Complex Specifications
Synthesizing Transducers from Complex Specifications
复制标题
DOI：
10.34727/2022/isbn.978-3-85448-053-2_36
复制
发表时间：
2022-08
期刊：
影响因子：
--
通讯作者：
Anvay Grover;Ruediger Ehlers;Loris D'antoni
中科院分区：
文献类型：
--
作者：
Anvay Grover;Ruediger Ehlers;Loris D'antoni
自动化字符串转换一直是程序合成的一个驱动应用。现有的合成器解决了这个问题，产生程序的领域特定语言（DSL），旨在简化合成，因此缺乏良好的形式属性。这种限制阻止了合成程序被用于验证应用（例如，以检查复杂的前置后置条件），并且由于合成器依赖于给定的DSL而使得合成器难以修改。我们提出了一种基于约束的方法来合成传感器，具有强大的封闭性和可判定性的模型。我们的方法处理三种类型的规范：输入-输出（i）示例，（ii）表示为正则语言的类型，以及（iii）在处理输入字符串时约束转换器可以修改多少字符的距离。我们的工作是第一个支持这种复杂的规格，它通过使用传感器的算法属性来生成可以使用现成的SMT求解器来解决的约束。我们的合成方法可以扩展到许多传感器模型，它可以使用，由于关闭属性的传感器，计算部分正确的传感器的维修。
Automating string transformations has been a driving application of program synthesis. Existing synthesizers that solve this problem produce programs in domain-specific languages (DSL) that are designed to simplify synthesis and therefore lack nice formal properties. This limitation prevents the synthesized programs from being used in verification applications (e.g., to check complex pre-post conditions) and makes the synthesizers hard to modify due to their reliance on the given DSL. We present a constraint-based approach to synthesizing transducers, a model with strong closure and decidability properties. Our approach handles three types of specifications: input-output (i) examples, (ii) types expressed as regular languages, and (iii) distances that bound how many characters the transducer can modify when processing an input string. Our work is the first to support such complex specifications and it does so by using the algorithmic properties of transducers to generate constraints that can be solved using off-the-shelf SMT solvers. Our synthesis approach can be extended to many transducer models and it can be used, thanks to closure properties of transducers, to compute repairs for partially correct transducers.