3 papers
cs.PL2025
CCR 2.0: High-level Reasoning for Conditional Refinements
Youngju Song, Minki Cho
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 unar…
cs.PL2022
Conditional Contextual Refinement (CCR)
Youngju Song, Minki Cho, Dongjae Lee +1
Contextual refinement (CR) is one of the standard notions of specifying open programs. CR has two main advantages: (i) (horizontal and vertical) compositionality that allows us to…
cs.PL2021
Abstraction Logic: The Marriage of Contextual Refinement and Separation Logic
Youngju Song, Minki Cho, Dongjae Lee +1
Contextual refinement and separation logics are successful verification techniques that are very different in nature. First, the former guarantees behavioral refinement between a c…