Portal de Periódicos da CAPES

A Program Logic for Bytecode

2005; Elsevier BV; Volume: 141; Issue: 1 Linguagem: Inglês

10.1016/j.entcs.2005.02.026

1571-0661

Fabian Yves Bannwart, Péter Müller,

Formal Methods in Verification

Program logics for bytecode languages such as Java bytecode or the .NET CIL can be used to apply Proof-Carrying Code concepts to bytecode programs and to verify correctness properties of bytecode programs. This paper presents a Hoare-style logic for a sequential bytecode kernel language similar to Java bytecode and CIL. The logic handles object-oriented features such as inheritance, dynamic method binding, and object structures with destructive updates, as well as unstructured control flow with jumps. It is sound and complete.