CCR: A marriage of refinement and separation logic.

Add to your list(s) Download to your calendar using vCal

• Youngju Song, MPI-SWS
• Wednesday 17 May 2023, 15:00-16:00
• SS03, Computer Laboratory.

If you have a question about this talk, please contact Ben Simner.

Much work in formal verification of low-level systems is based on one of two approaches: refinement or separation logic. These two approaches have complementary benefits: refinement supports the use of programs as specifications, as well as transitive composition of proofs, whereas separation logic supports conditional specifications, as well as modular ownership reasoning about shared state. In this talk, I will present Conditional Contextual Refinement (or CCR , for short), the first verification 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 simultaneously.

This talk is part of the bs630's list series.

This talk is included in these lists:

• SS03, Computer Laboratory

Note that ex-directory lists are not shown.