Symbolic finite state transducers: algorithms and applications
Symbolic finite state transducers: algorithms and applications
复制标题
DOI：
10.1145/2103656.2103674
复制
发表时间：
2012-01
影响因子：
0.8
通讯作者：
Margus Veanes;Pieter Hooimeijer;B. Livshits;D. Molnar;Nikolaj S. Bjørner
中科院分区：
文献类型：
--
作者：
Margus Veanes;Pieter Hooimeijer;B. Livshits;D. Molnar;Nikolaj S. Bjørner
有限自动机和有限转换器在软件工程中有广泛的应用，从正则表达式到规范语言。我们扩展这些经典的对象与符号字母表表示为参数理论。允许潜在的无限字母表使得这种表示比经典的有限转换器和字符串上的自动机严格地更一般和简洁。尽管如此，主要的操作，包括组合，检查换能器是单值的，和等价性检查单值符号有限换能器是有效的决策过程的背景理论。我们为这些操作提供了新的算法，并将组合扩展到用寄存器增强的符号换能器。我们的基本算法是不寻常的，因为它们是非建设性的，因此，我们还提供了一个单独的模型生成算法，可以快速找到反例的情况下，两个符号有限换能器是不等价的。该算法产生一个完整的可判定代数的符号传感器。与以前的工作不同，我们不需要任何语法限制的公式上的过渡，只有一个决策过程。在实践中，我们利用可满足性模理论（SMT）求解器的最新进展。我们展示了我们的技术在四个案例研究，涵盖了广泛的应用。我们的技术可以在大约一分钟内合成超过8,000字节的字符串前图像，我们发现我们的新编码在简洁性和分析速度方面明显优于以前的技术。
Finite automata and finite transducers are used in a wide range of applications in software engineering, from regular expressions to specification languages. We extend these classic objects with symbolic alphabets represented as parametric theories. Admitting potentially infinite alphabets makes this representation strictly more general and succinct than classical finite transducers and automata over strings. Despite this, the main operations, including composition, checking that a transducer is single-valued, and equivalence checking for single-valued symbolic finite transducers are effective given a decision procedure for the background theory. We provide novel algorithms for these operations and extend composition to symbolic transducers augmented with registers. Our base algorithms are unusual in that they are nonconstructive, therefore, we also supply a separate model generation algorithm that can quickly find counterexamples in the case two symbolic finite transducers are not equivalent. The algorithms give rise to a complete decidable algebra of symbolic transducers. Unlike previous work, we do not need any syntactic restriction of the formulas on the transitions, only a decision procedure. In practice we leverage recent advances in satisfiability modulo theory (SMT) solvers. We demonstrate our techniques on four case studies, covering a wide range of applications. Our techniques can synthesize string pre-images in excess of 8,000 bytes in roughly a minute, and we find that our new encodings significantly outperform previous techniques in succinctness and speed of analysis.