CRIS: The power of imagination in specification and verification
summary
CRIS introduces imaginary nondeterminism to let specifications include angelic choices and mix operational steps with separation logic, implemented on top of Iris and interaction trees. The tool proves contextual refinements, verifies a cell library example, cancels generated assume/guarantee boilerplate automatically, and supports CLight, concurrency, weak and C11-style memory models; several modules and an xlinked‑list end‑to‑end C→assembly verification are done and demos succeed, while some extensions remain in progress.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 1:03Imaginary specifications
- 6:43Cell library example
- 10:13Imaginary specs semantics
- 15:09Verifying main function
- 21:10Module proofs with refinement
- 26:06Atomicity and abstraction examples
- 31:27CRIS verification demo
- 35:40CRIS modularity and extensibility
- 47:24CRIS status and future
- 48:48Q&A
related talks
19mAn Iris Instance for Verifying CompCert C Programs
31mFormal Specification
22mDestabilizing Iris
21mThe New Verification Ecosystem that Supports RISC-V Verification fo...
15mCompiling with Continuations, Correctly
23mChisel 6 and beyond
20mMimIR: An Extensible and Type-Safe Intermediate Representation for the DSL Age
01h 06mVerifying a compiler through equational means