TY - GEN
T1 - Constraint-Based Relational Verification
AU - Unno, Hiroshi
AU - Terauchi, Tachio
AU - Koskinen, Eric
N1 - Funding Information:
Acknowledgments. We thank the anonymous reviewers for their suggestions. This work was supported by ONR grant # N00014-17-1-2787, JST ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), and JSPS KAKENHI Grant Numbers 17H01720, 18K19787, 19H04084, 20H04162, 20H05703, and 20K20625.
Publisher Copyright:
© 2021, The Author(s).
PY - 2021
Y1 - 2021
N2 - 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.
AB - 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.
KW - CEGIS
KW - Constraint solving
KW - Relational verification
UR - http://www.scopus.com/inward/record.url?scp=85113457381&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85113457381&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-81685-8_35
DO - 10.1007/978-3-030-81685-8_35
M3 - Conference contribution
AN - SCOPUS:85113457381
SN - 9783030816841
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 742
EP - 766
BT - Computer Aided Verification - 33rd International Conference, CAV 2021, Proceedings
A2 - Silva, Alexandra
A2 - Leino, K. Rustan
PB - Springer Science and Business Media Deutschland GmbH
T2 - 33rd International Conference on Computer Aided Verification, CAV 2021
Y2 - 20 July 2021 through 23 July 2021
ER -