Model Checking Information Flow in Reactive Systems

DOI10.1007/978-3-642-27940-9_12MaRDI QIDQ2891409zbMATH OpenOpenAlexFDO

Authors Rayna Dimitrova, Bernd Finkbeiner, Máté Kovács, Markus Rabe, Helmut Seidl

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

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Computing Information Flow Using Symbolic Model-Checking
• Model checking techniqes for the analysis of reactive systems
• scientific article; zbMATH DE number 5021521
• scientific article; zbMATH DE number 2182600
• Towards the hierarchical verification of reactive systems
• From model checking to equilibrium checking: reactive modules for rational verification

Cites work

• scientific article; zbMATH DE number 1500666 (Why is no real title available?)
• scientific article; zbMATH DE number 795590 (Why is no real title available?)
• A semantic framework for declassification and endorsement
• Alternating finite automata on -words
• An automata-theoretic approach to branching-time model checking
• Model Checking Knowledge and Linear Time: PSPACE Cases
• Model Checking on Trees with Path Equivalences
• Paralocks, role-based information flow control and beyond
• Preserving Secrecy Under Refinement
• Reasoning about infinite computations

Cited in

(11)

• CoCon: a conference management system with formally verified document confidentiality
• DeFi composability as MEV non-interference
• Model Checking on Trees with Path Equivalences
• Monitoring hyperproperties
• Compositional model checking for multi-properties
• Computing Information Flow Using Symbolic Model-Checking
• Synthesis from hyperproperties
• Model checking the observational determinism security property using PROMELA and SPIN
• Flavors of sequential information flow
• Information Flow Guided Synthesis
• A hybrid, dynamic logic for hybrid-dynamic information flow

Describes a project that uses

Uses Software

• Paragon

This page was built for publication: Model Checking Information Flow in Reactive Systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2891409)