Relational bytecode correlations

DOI10.1016/J.JLAP.2010.07.005MaRDI QIDQ710672zbMATH OpenOpenAlexFDO

Authors 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

non-interferenceprogram transformationsformalised program analysesproof-carrying coderelational proof systems

Mathematics Subject Classification ID

Theory of software (68N99)

Recommendations

• A Certified Lightweight Non-interference Java Bytecode Verifier
• A certified lightweight non-interference Java bytecode verifier
• scientific article; zbMATH DE number 1701360
• Lightweight bytecode verification
• Formalizing non-interference for a simple bytecode language in Coq

Cites work

• scientific article; zbMATH DE number 1948157 (Why is no real title available?)
• A Certified Lightweight Non-interference Java Bytecode Verifier
• A compositional natural semantics and Hoare logic for low-level languages
• A logic for information flow in object-oriented programs
• A semantic approach to secure information flow
• Abstract non-interference
• Automated soundness proofs for dataflow analyses and transformations via local rules
• Certification Using the Mobius Base Logic
• Discovering affine equalities using random interpretation
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• Formal verification of translation validators
• Information flow inference for ML
• Integration of a Security Type System into a Program Logic
• Interprocedurally Analyzing Polynomial Identities
• Isabelle/HOL. A proof assistant for higher-order logic
• Logic for Programming, Artificial Intelligence, and Reasoning
• On flow-sensitive security types
• Programming languages and systems. 4th Asian symposium, APLAS 2006, Sydney, Australia, November 8--10, 2006. Proceedings
• Proof optimization for partial redundancy elimination
• Relational Parametricity and Separation Logic
• Relational separation logic
• Semantic models for the security of sequential and concurrent programs
• Simple relational correctness proofs for static analyses and program transformations
• Stack-based access control and secure information flow
• Static Analysis
• Theoretical Computer Science
• Transforming out timing leaks
• Unwinding Conditions for Security in Imperative Languages
• Verification, Model Checking, and Abstract Interpretation

Cited in

(1)

• Constraint-based relational verification

Describes a project that uses

Uses Software

• CoVaC
• Isabelle/HOL

This page was built for publication: Relational bytecode correlations

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