Conditional Contextual Refinement (CCR): conditional, compositional and gradual specifications for open programs.

  • Date and time: Wednesday 13 October 2021, 1.30pm
  • Location: In-person (CSE082-083) or online (via Zoom)

Event details

Contextual refinement (CR) is one of the most natural ways of specifying an open program. For an open program P, we can give a more abstract program A as its specification and prove the contextual refinement between P and A, saying that P behaves like A under all contexts. An important advantage of CR is that one can horizontally and vertically decompose a large contextual refinement into many smaller ones, which allows compositional and gradual verification.

However, CR has a serious downside that it can only specify unconditional refinement. Specifically, CR quantifies over *all* contexts instead of those satisfying given user-specified conditions. Indeed, the unconditional quantification plays a key role in the full (i.e., horizontal and vertical) compositionality of CR, and finding a conditional yet fully compositional notion of refinement has been a long-standing open problem.

In this talk, I will introduce our solution to the open problem, called CCR (Conditional Contextual Refinement), and a next generation verification framework based on it, called CCR framework. The CCR framework supports rich conditions as in Iris, the state-of-the-art separation logic (e.g., mutually recursive, higher-order and resource-based conditions). Also, the CCR framework is fully formalized in Coq and its refinement proofs can be combined with CompCert, so that we can formally establish behavioral refinement from top-level abstract programs, all the way down to their assembly code.

Hosted by Simon Forster with guest speaker Professor Chung-Kil Hur.

Join on Zoom

Professor Chung-Kil Hur, Software Foundations Lab, Department of Computer Science and Engineering, Seoul National University

Contact us

Dr Dimitar Kazakov

Dr Dimitar Kazakov

Seminars organiser
+44 (0)1904 325676