Compositional Security-Preserving Refinement for Concurrent Imperative Programs

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

June 28, 2016

Abstract

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

Topics

Theories of Dependent_SIFUM_Refinement