Compositional Security-Preserving Refinement for Concurrent Imperative Programs

Toby Murray, Robert Sison, Edward Pierzchalski and Christine Rizkallah

28 June 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

Change history

[2016-08-19] Removed unused "stop" parameters from the sifum_refinement locale. (revision dbc482d36372) [2016-09-02] TobyM extended "simple" refinement theory to be usable for all bisimulations. (revision 547f31c25f60)

Depends On


Related Entries