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 language | English (US) |
---|---|
Pages (from-to) | 483-514 |
Number of pages | 32 |
Journal | Journal of Logic and Algebraic Programming |
Volume | 79 |
Issue number | 7 |
DOIs | |
State | Published - Oct 2010 |
Externally published | Yes |
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