Specification and Synthesized Implementation of Java Bytecode Verifier and Loader
Starting point: two “semi-formal” specifications
Background and Motivation
Why Formalize the Java Bytecode Verifier and Loader?
Information Flow
Java Virtual Machine
Java Concepts
Class Files
JVM Loading
Local and Global Consistency
Structure of the JVM
Bytecode Local Consistency Checks
A Dataflow Approach to Bytecode Verification
Data Flow Analysis
Intra-Procedural Data Flow Analysis
Instantiation of the DF Architecture
Lattice Construction: Formalization of JVM Primitive Types
Reference Types
JVM Type Categories
Subtype Assertions
Signature Assertions
Lattice Structure
Global Consistency
Consistent Assertion Sets
Typing Contexts
Lattice Theory
Lattice Constructions
Lattice for the JVM
Lg
LUB for Objects
No LUB in the Presence of Interfaces
Le
Transfer Functions
Example
Proving Transfer Functions Distributive
Object Initialization
Control Flow Graph
What did the designers of JVM Learn From COBOL?
Propagating the Types of Unexamined Variables
Constraint Solving
Applications
System Components
Data Flow Architecture in Specware
Formalization in Specware
Formalization
Refinement
Testing and Verification
Related Work
Email: goldberg@kestrel.edu
Home Page: http://www.kestrel.edu