Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
10328866 | Electronic Notes in Theoretical Computer Science | 2005 | 19 Pages |
Abstract
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Fabian Bannwart, Peter Müller,