Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP entry: Possibilistic Noninterference


view this post on Zulip Email Gateway (Aug 19 2022 at 08:46):

From: Tobias Nipkow <nipkow@in.tum.de>
Possibilistic Noninterference
Andrei Popescu and Johannes Hölzl
http://afp.sourceforge.net/entries/Possibilistic_Noninterference.shtml

We formalize a wide variety of Volpano/Smith-style noninterference notions for a
while language with parallel composition. We systematize and classify these
notions according to compositionality w.r.t. the language constructs.
Compositionality yields sound syntactic criteria (a.k.a. type systems) in a
uniform way.

An article http://www21.in.tum.de/~nipkow/pubs/cpp12.html about these proofs is
published in the proceedings of the conference Certified Programs and Proofs 2012

Enjoy!


Last updated: Apr 24 2024 at 20:16 UTC