CRIS: The Power of Imagination in Specification and Verification

This conference talk introduces CRIS (Contextual Refinement with Imaginary Specification), a novel verification tool that enhances program verification through the concept of imaginary specifications. Drawing a parallel to how imaginary numbers extend real numbers in mathematics, learn how imaginary specifications can simplify complex proofs by breaking them into more manageable steps. Discover how CRIS creates a unified framework that combines separation logic with pre/post conditions and program refinement with abstract programs. The presentation demonstrates how this approach enables elegant expression of traditionally difficult-to-specify properties, such as separation logic conditions involving IO events and logical atomicity. Presented by Chung-Kil Hur from Seoul National University at the CPP 2025 conference, this hour-long talk explores a groundbreaking approach to verification that promises to make complex program verification more accessible and effective.