Formal verification of language-based concurrent noninterference
From MaRDI portal
Recommendations
- Verification of fine-grain concurrent programs
- On verifying that a concurrent program satisfies a nondeterministic specification
- Verification of concurrent programs: The automata-theoretic framework
- Formal verification of concurrent programs with Read-write locks
- Specification and verification of concurrent programs through refinements
- Higher-order program verification and language-based security (extended abstract)
- Formalizing non-interference for a simple bytecode language in Coq
Cited in
(11)- A formally verified interpreter for a shell-like programming language
- CoCon: a conference management system with formally verified document confidentiality
- Formalizing probabilistic noninterference
- Abstract Certification of Global Non-interference in Rewriting Logic
- Proving concurrent noninterference
- Towards SOS meta-theory for language-based security
- Decidability and proof systems for language-based noninterference relations
- Self-composition by symbolic execution
- Unwinding Conditions for Security in Imperative Languages
- Relative security: (dis)proving resilience against semantic optimization vulnerabilities in Isabelle/HOL. Extended version
- Formalizing non-interference for a simple bytecode language in Coq
This page was built for publication: Formal verification of language-based concurrent noninterference
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5195249)
