Compositional Security-Preserving Refinement for Concurrent Imperative Programs

Toby Murray 🌐, Robert Sison, Edward Pierzchalski and Christine Rizkallah 🌐

June 28, 2016


The paper "Compositional Verification and Refinement of Concurrent Value-Dependent Noninterference" by Murray et. al. (CSF 2016) presents a compositional theory of refinement for a value-dependent noninterference property, defined in (Murray, PLAS 2015), for concurrent programs. This development formalises that refinement theory, and demonstrates its application on some small examples.
BSD License


Theories of Dependent_SIFUM_Refinement