BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:CCR: A marriage of refinement and separation logic. - Youngju Song
 \, MPI-SWS
DTSTART:20230517T140000Z
DTEND:20230517T150000Z
UID:TALK201232@talks.cam.ac.uk
CONTACT:Ben Simner
DESCRIPTION:Much work in formal verification of low-level systems is\nbase
 d on one of two approaches: refinement or separation logic. These two appr
 oaches have complementary benefits: refinement supports the use of program
 s as specifications\, as well as transitive composition of proofs\, wherea
 s separation logic supports conditional specifications\, as well as modula
 r ownership reasoning about shared state. In this talk\, I will present Co
 nditional Contextual Refinement (or CCR\, for short)\, the first verificat
 ion system to not only combine refinement and separation logic in a single
  framework but also to truly marry them together into a unified mechanism 
 enjoying all the benefits of refinement and separation logic simultaneousl
 y.
LOCATION:SS03\, Computer Laboratory
END:VEVENT
END:VCALENDAR