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.
- 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)