Formalizing non-interference for a simple bytecode language in Coq
From MaRDI portal
Publication:931434
DOI10.1007/s00165-007-0055-2zbMath1151.68633OpenAlexW2156734947MaRDI QIDQ931434
Publication date: 25 June 2008
Published in: Formal Aspects of Computing (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s00165-007-0055-2
Formal methods for securityInteractive theorem provingModular specificationProgramming language analysis
Related Items
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Java bytecode verification: Algorithms and formalizations
- A semantic approach to secure information flow
- Verified bytecode verifiers.
- A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L
- Types, bytes, and separation logic
- Certification of programs for secure information flow
- Stack-based access control and secure information flow
- Fundamental Approaches to Software Engineering
- A formulation of the simple theory of types
- Verification, Model Checking, and Abstract Interpretation