认证符号有限变换器：形式化及其在字符串分析中的应用
形式语言与自动机理论
2025-09-16 v2
摘要
有限自动机（FA）是编程语言领域的基本组件。例如，正则表达式——这在诸如 JavaScript 和 Python 的语言中至关重要——常常使用 FA 实现。有限变换器（FT）通过启用将输入字符串转换为输出字符串的功能，为涵盖识别和转换的更具表达力的框架提供支持。尽管在诸如 Coq 和 Isabelle/HOL 等证明辅助器中对 FA 的各种形式化实现，但这些实现往往在现实场景的适用性方面不足。更实用的做法是对符号 FA 和 FT 进行形式化，其中转换标签是符号的且可能是无限的。虽然 CertiStr 研究了符号 FA 的形式化，但在交互式证明辅助器中对符号 FT 的形式化仍然 largely 未探索，due to 增加的复杂性挑战。本文旨在在 Isabelle/HOL 框架中形式化符号 FT。该形式化是细化基的，并且设计用于可扩展 various 符号转换标签表示。为评估其性能，我们将形式化的符号 FT 应用于 SMT 字符串求解器以建模替换操作。实验结果表明，形式化的符号变换器能够高效有效地解决带有替换操作的字符串约束。
关键词
引用
@article{arxiv.2504.07203,
title = {Certified Symbolic Finite Transducers: Formalization and Applications to String Analysis},
author = {Shuanglong Kan and Anthony W. Lin},
journal= {arXiv preprint arXiv:2504.07203},
year = {2025}
}
备注
Conference