Compositional Security-Preserving Refinement for Concurrent Imperative Programs

 

Title: Compositional Security-Preserving Refinement for Concurrent Imperative Programs
Authors: Toby Murray, Robert Sison, Edward Pierzchalski and Christine Rizkallah
Submission date: 2016-06-28
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.
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)
BibTeX:
@article{Dependent_SIFUM_Refinement-AFP,
  author  = {Toby Murray and Robert Sison and Edward Pierzchalski and Christine Rizkallah},
  title   = {Compositional Security-Preserving Refinement for Concurrent Imperative Programs},
  journal = {Archive of Formal Proofs},
  month   = jun,
  year    = 2016,
  note    = {\url{http://isa-afp.org/entries/Dependent_SIFUM_Refinement.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Depends on: Dependent_SIFUM_Type_Systems