[isabelle] new in the AFP: Refinement for Concurrent Imperative Programs



A second AFP entry was published today, details below. And that makes five entries in the past week! Keep them coming!!

Larry Paulson


Compositional Security-Preserving Refinement for Concurrent Imperative Programs

Author: Toby Murray, Robert Sison, Edward Pierzchalski and Christine Rizkallah

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.

https://www.isa-afp.org/entries/Dependent_SIFUM_Refinement.shtml



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.