Noninterfering schedulers when possibilistic noninterference implies probabilistic noninterference

Andrei Popescu, Johannes Hölzl, Tobias Nipkow

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

5 Scopus citations

Abstract

We develop a framework for expressing and analyzing the behavior of probabilistic schedulers. There, we define noninterfering schedulers by a probabilistic interpretation of Goguen and Meseguer's seminal notion of noninterference. Noninterfering schedulers are proved to be safe in the following sense: if a multi-threaded program is possibilistically noninterfering, then it is also probabilistically noninterfering when run under this scheduler.

Original languageEnglish
Title of host publicationAlgebra and Coalgebra in Computer Science - 5th International Conference, CALCO 2013, Proceedings
PublisherSpringer Verlag
Pages236-252
Number of pages17
ISBN (Print)9783642402050
DOIs
StatePublished - 2013
Event5th International Conference on Algebra and Coalgebra in Computer Science, CALCO 2013 - Warsaw, Poland
Duration: 3 Sep 20136 Sep 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8089 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference5th International Conference on Algebra and Coalgebra in Computer Science, CALCO 2013
Country/TerritoryPoland
CityWarsaw
Period3/09/136/09/13

Fingerprint

Dive into the research topics of 'Noninterfering schedulers when possibilistic noninterference implies probabilistic noninterference'. Together they form a unique fingerprint.

Cite this