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