Constraint-Based Relational Verification

Hiroshi Unno*, Tachio Terauchi, Eric Koskinen

*この研究の対応する著者

研究成果: Conference contribution

1 被引用数 (Scopus)

抄録

In recent years they have been numerous works that aim to automate relational verification. Meanwhile, although Constrained Horn Clauses (CHCs ) empower a wide range of verification techniques and tools, they lack the ability to express hyperproperties beyond k-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 called pfwCSP where constraints are represented as clauses modulo first-order theories over predicate variables of three kinds: ordinary, well-founded, or functional. This generalization over CHCs permits 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 appropriate schedulers (or alignment) that dictate when and which program copies move. To solve problems in this new language, we present a constraint solving method for pfwCSP based on stratified CounterExample-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.

本文言語English
ホスト出版物のタイトルComputer Aided Verification - 33rd International Conference, CAV 2021, Proceedings
編集者Alexandra Silva, K. Rustan Leino
出版社Springer Science and Business Media Deutschland GmbH
ページ742-766
ページ数25
ISBN(印刷版)9783030816841
DOI
出版ステータスPublished - 2021
イベント33rd International Conference on Computer Aided Verification, CAV 2021 - Virtual, Online
継続期間: 2021 7 202021 7 23

出版物シリーズ

名前Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
12759 LNCS
ISSN(印刷版)0302-9743
ISSN(電子版)1611-3349

Conference

Conference33rd International Conference on Computer Aided Verification, CAV 2021
CityVirtual, Online
Period21/7/2021/7/23

ASJC Scopus subject areas

  • 理論的コンピュータサイエンス
  • コンピュータ サイエンス(全般)

フィンガープリント

「Constraint-Based Relational Verification」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル