CTL+FO verification as constraint solving
CTL+FO verification as constraint solving
复制标题
CTL FO 验证作为约束求解
作者：
Tewodros A. Beyene;Marc Brockschmidt;A. Rybalchenko
表达程序正确性通常需要在整个执行（的不同分支）中关联程序数据。这些属性可以用CTL+FO来表示，这是一种允许混合时间和一阶量化的逻辑。判定程序是否满足CTL+FO性质是一个具有挑战性的问题，需要同时进行时间和数据推理。时态量词需要发现不变量和排序函数，而一阶量词需要实例化技术。本文提出了一种基于约束的CTL+FO性质自动证明方法。我们的方法使时间和一阶量化之间的相互作用明确的约束编码，结合递归和存在量化。通过将此约束编码与现成的求解器相结合，我们获得了CTL+FO的自动验证器。
Expressing program correctness often requires relating program data throughout (different branches of) an execution. Such properties can be represented using CTL+FO, a logic that allows mixing temporal and first-order quantification. Verifying that a program satisfies a CTL+FO property is a challenging problem that requires both temporal and data reasoning. Temporal quantifiers require discovery of invariants and ranking functions, while first-order quantifiers demand instantiation techniques. In this paper, we present a constraint-based method for proving CTL+FO properties automatically. Our method makes the interplay between the temporal and first-order quantification explicit in a constraint encoding that combines recursion and existential quantification. By integrating this constraint encoding with an off-the-shelf solver we obtain an automatic verifier for CTL+FO.
DOI：
10.1145/1920261.1920300
发表时间：
2010-12
期刊：
--
影响因子：
--
作者：
J. Heusser;P. Malacaria
通讯作者：
J. Heusser;P. Malacaria
解决存在量化的喇叭子句
DOI：
10.1007/978-3-642-39799-8_61
发表时间：
2013
期刊：
影响因子：
--
作者：
Tewodros A. Beyene;Corneliu Popeea;Andrey Rybalchenko
通讯作者：
Andrey Rybalchenko