Predicate Abstraction and CEGAR for $\nu \mathrm {HFL}_\mathbb {Z}$ Validity Checking
No abstract available.
Related papers
- A New Refinement Type System for Automated $\nu \text {HFL}_\mathbb {Z}$ Validity Checking APLAS 2020
- Predicate abstraction and CEGAR for higher-order model checking PLDI 2011
- HFL(Z) Validity Checking for Automated Program Verification POPL 2023
- Predicate Abstraction and CEGAR for Disproving Termination of Higher-Order Functional Programs CAV 2015
- Gazer-Theta: LLVM-based Verifier Portfolio with BMC/CEGAR (Competition Contribution) TACAS 2021
- Constraint-Based Relational Verification CAV 2021
- A Type-Based HFL Model Checking Algorithm APLAS 2019
- Higher-Order Program Verification via HFL Model Checking ESOP 2018