Constraint-based relational verification
From MaRDI portal
Publication:832229
DOI10.1007/978-3-030-81685-8_35zbMath1493.68125arXiv2106.02628OpenAlexW3186533773MaRDI QIDQ832229
Hiroshi Unno, Eric Koskinen, Tachio Terauchi
Publication date: 25 March 2022
Full work available at URL: https://arxiv.org/abs/2106.02628
Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (4)
Constraint-based relational verification ⋮ Decision tree learning in CEGIS-based termination analysis ⋮ Certified verification of relational properties ⋮ RHLE: modular deductive verification of relational \(\forall \exists\) properties
Uses Software
Cites Work
- Unnamed Item
- Relational bytecode correlations
- Constraint-based relational verification
- Predicate abstraction and CEGAR for disproving termination of higher-order functional programs
- Algorithms for model checking HyperLTL and HyperCTL\(^*\)
- 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
- Simple relational correctness proofs for static analyses and program transformations
- Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification
- Towards Modularly Comparing Programs Using Automated Theorem Provers
- Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs
- Ranking Templates for Linear Loops
- Dependent types from counterexamples
- A Data Driven Approach for Algebraic Loop Invariants
- Hypercollecting semantics and its application to static analysis of information flow
- An Abstract Domain to Infer Ordinal-Valued Ranking Functions
- Static Analysis
- Tools and Algorithms for the Construction and Analysis of Systems
- 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
This page was built for publication: Constraint-based relational verification
