Constraint-based relational verification

DOI10.1007/978-3-030-81685-8_35zbMATH Open1493.68125arXiv2106.02628OpenAlexW3186533773MaRDI QIDQ832229FDOQ832229

Authors: Hiroshi Unno, Tachio Terauchi, Eric Koskinen 

Publication date: 25 March 2022

Abstract: 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.

Full work available at URL: https://arxiv.org/abs/2106.02628

Recommendations

• Relational verification through Horn clause transformation
• Automating induction for solving Horn clauses
• Predicate pairing with abstraction for relational verification
• Predicate pairing for program verification
• Exploiting synchrony and symmetry in relational verification

zbMATH Keywords

constraint solvingCEGISrelational verification

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs
• Title not available (Why is that?)
• Tools and Algorithms for the Construction and Analysis of Systems
• An Abstract Domain to Infer Ordinal-Valued Ranking Functions
• Simple relational correctness proofs for static analyses and program transformations
• Towards Modularly Comparing Programs Using Automated Theorem Provers
• A Data Driven Approach for Algebraic Loop Invariants
• Static Analysis
• Relational bytecode correlations
• Dependent types from counterexamples
• Algorithms for model checking HyperLTL and HyperCTL\(^*\)
• Predicate abstraction and CEGAR for disproving termination of higher-order functional programs
• Automating induction for solving Horn clauses
• Relaxed Stratification: A New Approach to Practical Complete Predicate Refinement
• Horn Clause Solvers for Program Verification
• Learning refinement types
• Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification
• Ranking Templates for Linear Loops
• Hypercollecting semantics and its application to static analysis of information flow
• ICE-based refinement type discovery for higher-order functional programs
• Syntax-guided termination analysis
• Exploiting synchrony and symmetry in relational verification
• Verifying hyperliveness
• Property directed self composition
• Automated hypersafety verification
• Overfitting in synthesis: theory and practice
• Constraint-based relational verification

Cited In (9)

• Constraint-based relational verification
• Decision tree learning in CEGIS-based termination analysis
• Exploiting synchrony and symmetry in relational verification
• Software Verification of Hyperproperties Beyond k-Safety
• Maintaining state constraints in relational databases: a proof theoretic basis
• RHLE: modular deductive verification of relational \(\forall \exists\) properties
• Certified verification of relational properties
• Static Analysis
• Lockstep composition for unbalanced loops

Uses Software

• z3
• HMC
• SeaHorn
• Spacer
• CoVaC
• MoCHi
• JayHorn

This page was built for publication: Constraint-based relational verification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q832229)