Predicate Abstraction and CEGAR for Disproving Termination of Higher-Order Functional Programs
No abstract available.
Related papers
- Automatically disproving fair termination of higher-order functional programs ICFP 2016
- Predicate abstraction and CEGAR for higher-order model checking PLDI 2011
- Predicate Abstraction and CEGAR for $\nu \mathrm {HFL}_\mathbb {Z}$ Validity Checking SAS 2020
- Gazer-Theta: LLVM-based Verifier Portfolio with BMC/CEGAR (Competition Contribution) TACAS 2021
- AProVE: Proving and Disproving Termination of Memory-Manipulating C Programs - (Competition Contribution) TACAS 2017
- Size-based termination of higher-order rewriting JFP 2018
- Higher-Order LCTRSs and Their Termination ESOP 2024
- Termination Analysis of Higher-Order Functional Programs APLAS 2005