Relational bytecode correlations

DOI10.1016/j.jlap.2010.07.005zbMath1204.68070OpenAlexW2007975752MaRDI QIDQ710672

Lennart Beringer

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

zbMATH Keywords

program transformationsnon-interferenceformalised program analysesproof-carrying coderelational proof systems

Mathematics Subject Classification ID

Theory of software (68N99)

Related Items (1)

Constraint-based relational verification

Uses Software

• Isabelle/HOL
• CoVaC

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

This page was built for publication: Relational bytecode correlations