CRIS: The Power of Imagination in Hybrid Verification
summary
Introduces CRIS, a framework that extends CCR with imaginary specifications—specs that intermix executable code and separation-logic assertions—to prove contextual refinement when some modules remain unverified and may perform I/O or diverge. Demonstrates a cell example where inlining specs lets a client and library compose while undefined behavior on the abstract side makes certain interferences vacuously safe. Provides full mechanization and proofs mechanized in Rocq, with artifacts available and evaluated.
AI-written summary · about
chapters (9)
- 0:00CRIS and hybrid verification
- 1:50Limitations of pre/post specs
- 3:54Imaginary specifications in CRIS
- 6:43Cell library verification with CRIS
- 7:24Refinement for main module
- 11:20Core reasoning and simulation rules
- 13:28CRIS summary and novelty
- 14:54Future directions and follow-ups
- 15:38Q&A on non-termination