Conditional Contextual Refinement (CCR): conditional, compositional and gradual specifications for open programs.
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.