ILC: A Foundation for Automated Reasoning About Pointer Programs
No abstract available.
Related papers
- RefinedC: automating the foundational verification of C code with refined ownership types PLDI 2021
- Mostly-automated verification of low-level programs in computational separation logic PLDI 2011
- Foundations for Entailment Checking in Quantitative Separation Logic ESOP 2022
- RefinedRust: A Type System for High-Assurance Verification of Rust Programs PLDI 2024
- Velvet: A Foundational Multi-modal Verifier for Imperative Programs in Lean CAV 2026
- ILC: a calculus for composable, computational cryptography PLDI 2019
- Generically Automating Separation Logic by Functors, Homomorphisms, and Modules POPL 2025
- Foundational Multi-Modal Program Verifiers POPL 2026