@inproceedings{pop-pos,
 title = "Proving Possibilistic, Probabilistic Noninterference",
 author = "Andrei Popescu and Johannes H{\"{o}}lzl and Tobias Nipkow",
 booktitle = {Certified Programs and Proofs (CPP) '12},
 year = {2012},
 pages = {},
 }


