Formalizing Probabilistic Noninterference

DOI10.1007/978-3-319-03545-1_17zbMath1426.68287OpenAlexW1484822807MaRDI QIDQ2938053

Johannes Hölzl, Tobias Nipkow, Andrei Popescu

Publication date: 13 January 2015

Published in: Certified Programs and Proofs (Search for Journal in Brave)

Full work available at URL: https://eprints.mdx.ac.uk/15369/1/PROB.pdf

Mathematics Subject Classification ID

Theory of programming languages (68N15) Formalization of mathematics in connection with theorem provers (68V20)

Related Items (3)

A formalized general theory of syntax with bindings ⋮ Markov chains and Markov decision processes in Isabelle/HOL ⋮ A formalized general theory of syntax with bindings: extended version

Uses Software

• Isabelle

Cites Work

• Unnamed Item
• Proofs of randomized algorithms in Coq
• Bisimulation through probabilistic testing
• Isabelle/HOL. A proof assistant for higher-order logic
• Noninterference for concurrent programs and thread systems
• Probabilistic guarded commands mechanized in HOL
• Noninterfering Schedulers
• Verifying pCTL Model Checking
• Secure information flow by self-composition
• Abstraction, Refinement and Proof for Probabilistic Systems
• Proving Concurrent Noninterference
• Formal certification of code-based cryptographic proofs
• Practical Probability: Applying pGCL to Lattice Scheduling
• Theoretical Aspects of Computing – ICTAC 2005
• Perspectives of System Informatics

This page was built for publication: Formalizing Probabilistic Noninterference