CCR 2.0: High-level Reasoning for Conditional Refinements

TL;DR

This paper advances the CCR framework for formal verification by introducing CCR 2.0, which integrates refinement, unary, and relational separation logics, providing more powerful reasoning principles.

Contribution

The paper develops CCR 2.0, a novel extension of CCR 1.0, with improved reasoning principles and the ability to fuse multiple verification approaches into a unified mechanism.

Findings

Formalized CCR 2.0 in Rocq

Enhanced reasoning principles for CCR 2.0

Unified benefits of refinement and separation logics

Abstract

In recent years, great progress has been made in the field of formal verification for low-level systems. Many of them are based on one of two popular approaches: refinement or unary separation logic. These two approaches are very different in nature and offer complementary benefits in compositionality. Recently, to fuse these benefits into a single unified mechanism, a new approach called Conditional Contextual Refinement (CCR 1.0 for short) was proposed. In this paper, we advance CCR 1.0 and provide novel and intuitive reasoning principles, resulting in CCR 2.0. Achieving this goal was challenging due to non-trivial counterexamples which necessitated elegant changes to the model of CCR 1.0. On top of CCR 2.0, we show how to fuse the benefits of refinement, unary separation logic, and also relational separation logic. Our results are formalized in Rocq.