Relational bytecode correlations

DOI10.1016/J.JLAP.2010.07.005zbMATH Open1204.68070OpenAlexW2007975752MaRDI QIDQ710672FDOQ710672

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

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

zbMATH Keywords

non-interferenceprogram transformationsformalised program analysesproof-carrying coderelational proof systems

Mathematics Subject Classification ID

Theory of software (68N99)

Cites Work

• Isabelle/HOL. A proof assistant for higher-order logic
• Transforming out timing leaks
• Information flow inference for ML
• Programming languages and systems. 4th Asian symposium, APLAS 2006, Sydney, Australia, November 8--10, 2006. Proceedings
• Formal verification of translation validators
• A semantic approach to secure information flow
• Discovering affine equalities using random interpretation
• Formal certification of a compiler back-end or
• A compositional natural semantics and Hoare logic for low-level languages
• Stack-based access control and secure information flow
• Abstract non-interference
• Relational separation logic
• A logic for information flow in object-oriented programs
• Simple relational correctness proofs for static analyses and program transformations
• Title not available (Why is that?)
• Semantic models for the security of sequential and concurrent programs
• Relational Parametricity and Separation Logic
• Automated soundness proofs for dataflow analyses and transformations via local rules
• Certification Using the Mobius Base Logic
• Integration of a Security Type System into a Program Logic
• On flow-sensitive security types
• 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
• Static Analysis
• Proof optimization for partial redundancy elimination

Cited In (1)

• Constraint-based relational verification

Uses Software

• Isabelle/HOL
• CoVaC

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)