重写理论中基于构造函数的可达性逻辑
A Constructor-Based Reachability Logic for Rewrite Theories
摘要：
可达性逻辑作为程序的语言类属逻辑，已被应用于$\mathbb{K}$重写基于规则的语言定义。为了能够验证不仅是代码，而且分布式系统设计，一个新的重写理论通用可达性逻辑，并证明了广泛的重写理论的声音。通过基于构造器的语义统一、匹配和可满足性过程，提高了逻辑的自动化程度。开发了新的方法来证明可能永远不会终止的分布式系统的不变量，并提出了一个原型实现的实验，说明了新的证明方法。
英文摘要：
Reachability logic has been applied to $\mathbb{K}$ rewrite-rule-based language definitions as a language-generic logic of programs. To be able to verify not just code but also distributed system designs, a new rewrite-theory-generic reachability logic is presented and proved sound for a wide class of rewrite theories. The logic's automation is increased by means of constructor-based semantic unification, matching, and satisfiability procedures. New methods for proving invariants of possibly never terminating distributed systems are developed, and experiments with a prototype implementation illustrating the new proof methods are presented.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
