Compositional Security-Preserving Refinement for Concurrent Imperative Programs

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

June 28, 2016

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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


September 2, 2016
TobyM extended "simple" refinement theory to be usable for all bisimulations. (revision 547f31c25f60)
August 19, 2016
Removed unused "stop" parameters from the sifum_refinement locale. (revision dbc482d36372)


Session Dependent_SIFUM_Refinement