Constraint-Based Relational Verification
Constraint-Based Relational Verification
复制标题
基于约束的关系验证
DOI：
10.1007/978-3-030-81685-8_35
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Koskinen Eric
中科院分区：
文献类型：
--
作者：
Unno Hiroshi;Terauchi Tachio;Koskinen Eric
近年来，他们已经有许多作品，旨在自动化关系验证。同时，尽管约束Horn子句（）赋予了广泛的验证技术和工具，但它们缺乏表达超越k-安全性的超性质的能力，例如广义不干涉和co-termination。我们首先介绍了一类新的谓词约束满足问题称为约束表示为子句模一阶理论的谓词变量的三种：普通的，有根据的，或功能。这种概括过度允许任意（即，可能非Horn）子句、良好基础约束、功能约束，并且能够表达这些关系验证问题。我们的方法使我们能够表达和自动验证需要非平凡的问题实例（即，非顺序和非锁步）自组合，通过自动推断适当的标记（或对齐）来指示何时以及哪个程序副本移动。为了解决这个新语言中的问题，我们提出了一种约束求解方法，基于分层反例引导归纳合成（CEGIS）的普通，良好的基础，和功能predictions.We实现了所提出的框架，并取得了可喜的成果，在各种关系验证问题，超出了以前的验证框架的范围。
In recent years they have been numerous works that aim to automate relational verification. Meanwhile, although Constrained Horn Clauses () empower a wide range of verification techniques and tools, they lack the ability to express hyperproperties beyondk-safety such as generalized non-interference and co-termination.This paper describes a novel and fully automated constraint-based approach to relational verification. We first introduce a new class of predicate Constraint Satisfaction Problems calledwhere constraints are represented as clauses modulo first-order theories over predicate variables of three kinds: ordinary, well-founded, or functional. This generalization overpermits arbitrary (i.e., possibly non-Horn) clauses, well-foundedness constraints, functionality constraints, and is capable of expressing these relational verification problems. Our approach enables us to express and automatically verify problem instances that require non-trivial (i.e., non-sequential and non-lock-step) self-composition by automatically inferring appropriateschedulers(oralignment) that dictate when and which program copies move. To solve problems in this new language, we present a constraint solving method forbased onstratifiedCounterExample-Guided Inductive Synthesis (CEGIS) of ordinary, well-founded, and functional predicates.We have implemented the proposed framework and obtained promising results on diverse relational verification problems that are beyond the scope of the previous verification frameworks.