CRIS (Contextual Refinement with Imaginary Specifications)

CRIS (Contextual Refinement with Imaginary Specifications)

CRIS is a Rocq framework for hybrid verification based on imaginary specifications, which mix executable code with ownership assertions.

[GitHub] [paper]

Paper

CRIS: The Power of Imagination in Hybrid Verification
Yonghee Kim, Taeyoung Yoon, Sanghyun Yi, Jaehyung Lee, Soonwon Moon, Yeji Han, Seonho Lee, Taeyoung Rhee, Yujin Im, Donghyun Nam, Jieung Kim, and Chung-Kil Hur.
Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2026), Proc. ACM Program. Lang. 10, Article 239, June 2026.
[paper] [publisher]

Events

Program Verification Workshop 2026
July 28–30, 2026.
A three-day workshop on CRIS, progressing from Hoare Logic and Separation Logic to full verification of a linked-list program.