Relational bytecode correlations

Lennart Beringer

Research output: Contribution to journalArticlepeer-review

2 Scopus citations

Abstract

We present a calculus for tracking equality relationships between values through pairs of bytecode programs.Thecalculusmay serve as a certificationmechanismfor non-interference, a well-known program property in the field of language-based security, and code transformations. Contrary to previous type systems for non-interference, no restrictions are imposed on the control flow structure of programs. Objects, static and virtual methods are included, and heap-local reasoning is supported by frame rules. In combination with polyvariance, the latter enable the modular verification of programs over heap-allocated data structures, which we illustrate by verifying and comparing different implementations of list copying. The material is based on a complete formalisation in Isabelle/HOL.

Original languageEnglish (US)
Pages (from-to)483-514
Number of pages32
JournalJournal of Logic and Algebraic Programming
Volume79
Issue number7
DOIs
StatePublished - Oct 2010
Externally publishedYes

All Science Journal Classification (ASJC) codes

  • Software
  • Theoretical Computer Science
  • Logic
  • Computational Theory and Mathematics

Keywords

  • Formalised program analyses
  • Non-interference
  • Program transformations
  • Proof-carrying code
  • Relational proof systems

Fingerprint

Dive into the research topics of 'Relational bytecode correlations'. Together they form a unique fingerprint.

Cite this