BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:CRIS: The power of imagination in specification and verification -
  Gil Hur (Seoul National University)
DTSTART:20250304T130000Z
DTEND:20250304T140000Z
UID:TALK229090@talks.cam.ac.uk
CONTACT:Ioannis Markakis
DESCRIPTION:Just as imaginary numbers extend real numbers and simplify cer
 tain mathematical proofs\, we introduce the concept of imaginary specifica
 tions to enhance program verification. In mathematics\, imaginary numbers 
 enable expressing intermediate steps that cannot be captured using real nu
 mbers alone\, offering natural proof decomposition that reduces complex pr
 oofs into simpler\, more manageable steps. Similarly\, our work introduces
  imaginary specifications in program verification through CRIS (Contextual
  Refinement with Imaginary Specification)\, our novel verification tool.\n
 \nCRIS with imaginary specifications provides a unified framework to inher
 ently marry two fundamental approaches to program verification: separation
  logic with pre/post conditions as specifications\, and program refinement
  with abstract programs as specifications. This unification not only enabl
 es proof simplification via proof decomposition but also enables elegant e
 xpression of hard-to-express properties\, such as separation logic conditi
 ons involving IO events and logical atomicity—properties that traditiona
 lly require intricate mechanisms or are difficult to specify.
LOCATION:SS03\, Computer Laboratory
END:VEVENT
END:VCALENDAR