Model Checking Information Flow in Reactive Systems
From MaRDI portal
Publication:2891409
DOI10.1007/978-3-642-27940-9_12zbMath1326.68182OpenAlexW1866799138MaRDI QIDQ2891409
Markus N. Rabe, Helmut Seidl, Rayna Dimitrova, Máté Kovács, Bernd Finkbeiner
Publication date: 15 June 2012
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: http://eprints.whiterose.ac.uk/156479/7/vmcai12.pdf
Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Temporal logic (03B44)
Related Items
Flavors of sequential information flow ⋮ Model checking the observational determinism security property using PROMELA and SPIN ⋮ Compositional model checking for multi-properties ⋮ Monitoring hyperproperties ⋮ CoCon: a conference management system with formally verified document confidentiality ⋮ Synthesis from hyperproperties
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Alternating finite automata on \(\omega\)-words
- Reasoning about infinite computations
- A Semantic Framework for Declassification and Endorsement
- Preserving Secrecy Under Refinement
- Paralocks
- An automata-theoretic approach to branching-time model checking
- Model Checking Knowledge and Linear Time: PSPACE Cases
- Model Checking on Trees with Path Equivalences