Relational bytecode correlations
From MaRDI portal
Publication:710672
DOI10.1016/j.jlap.2010.07.005zbMath1204.68070MaRDI QIDQ710672
Publication date: 22 October 2010
Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.jlap.2010.07.005
program transformations; non-interference; formalised program analyses; proof-carrying code; relational proof systems
68N99: Theory of software
Related Items
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Proof optimization for partial redundancy elimination
- A compositional natural semantics and Hoare logic for low-level languages
- Relational separation logic
- A semantic approach to secure information flow
- Isabelle/HOL. A proof assistant for higher-order logic
- Programming languages and systems. 4th Asian symposium, APLAS 2006, Sydney, Australia, November 8--10, 2006. Proceedings
- Discovering affine equalities using random interpretation
- Formal verification of translation validators
- Simple relational correctness proofs for static analyses and program transformations
- Abstract non-interference
- Certification Using the Mobius Base Logic
- Integration of a Security Type System into a Program Logic
- Stack-based access control and secure information flow
- Transforming out timing leaks
- Information flow inference for ML
- Automated soundness proofs for dataflow analyses and transformations via local rules
- Formal certification of a compiler back-end or
- On flow-sensitive security types
- A logic for information flow in object-oriented programs
- Theoretical Computer Science
- Interprocedurally Analyzing Polynomial Identities
- Unwinding Conditions for Security in Imperative Languages
- Logic for Programming, Artificial Intelligence, and Reasoning
- Verification, Model Checking, and Abstract Interpretation
- A Certified Lightweight Non-interference Java Bytecode Verifier
- Relational Parametricity and Separation Logic
- Static Analysis
