University of Cambridge > > bs630's list > CCR: A marriage of refinement and separation logic.

CCR: A marriage of refinement and separation logic.

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2024, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity