A New Refinement Type System for Automated $\nu \text {HFL}_\mathbb {Z}$ Validity Checking
No abstract available.
Related papers
- Predicate Abstraction and CEGAR for $\nu \mathrm {HFL}_\mathbb {Z}$ Validity Checking SAS 2020
- HFL(Z) Validity Checking for Automated Program Verification POPL 2023
- Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System ICFP 2024
- Higher-Order Property-Directed Reachability ICFP 2023
- A Type-Based HFL Model Checking Algorithm APLAS 2019
- Higher-Order Program Verification via HFL Model Checking ESOP 2018
- StreamLAB: Stream-based Monitoring of Cyber-Physical Systems CAV 2019
- LiquidHaskell: experience with refinement types in the real world Haskell 2014