Destabilizing Iris
summary
Adds Daenerys to Iris: a reworked resource layer that introduces unstable resources and an explicit frame modality, plus an unstable points-to and a logic-level heap-dependent expression assertions form of E ↦ v. Proves a correspondence that lets SMT-style first-order formulas discharge these assertions, implements the redesign as a fork mechanized in Rock, and evaluates on case studies (including examples beyond plain Iris or Viper). Artifacts and reproducible evaluation are available.
AI-written summary · about
chapters (7)
- 0:00Introduction
- 3:53Heap dependent expressions
- 7:45Daenerys and unstable resources
- 10:17Redesigning framing
- 12:00Connecting to SMT solvers
- 15:10Case studies
- 15:40Q&A
related talks
19mAn Iris Instance for Verifying CompCert C Programs
27mR Melts Brains -- An IR for First-Class Environments and Lazy Effectful Arguments
18mGraph IRs for Impure Higher-Order Languages: Making Aggressive Optimizations Af...
01h 03mCRIS: The power of imagination in specification and verification
14mScala Step-by-Step — Soundness for DOT with Step-Indexed Logical Relations in Iris
20mMimIR: An Extensible and Type-Safe Intermediate Representation for the DSL Age
20mFirst-class Algebraic Presentations with Elaborator Reflection (Extended Abstract)
01h 06mKeynote – Edwin Brady