Parameterized Recursive Refinement Types for Automated Program Verification
No abstract available.
Related papers
- Type-based data structure verification PLDI 2009
- Thrust: A Prophecy-Based Refinement Type System for Rust PLDI 2025
- Automated Inductive Verification of Parameterized Protocols CAV 2001
- Automated Software Verification of Hyperliveness TACAS 2024
- Refinement reflection: complete verification with SMT POPL 2018
- Automated Parameterized Verification of CRDTs CAV 2019
- Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System ICFP 2024
- RefinedC: automating the foundational verification of C code with refined ownership types PLDI 2021