Abstract
An annotation of java virtual machine code with types to enable a one-pass verification of well-typedness was proposed. It contains the lightweight bytecode verifier as an executable functional program. The lightweight bytecode verifier builds on the existing specification of the whole μJava language.
| Original language | English |
|---|---|
| Pages (from-to) | 1133-1151 |
| Number of pages | 19 |
| Journal | Concurrency and Computation: Practice and Experience |
| Volume | 13 |
| Issue number | 13 |
| DOIs | |
| State | Published - Nov 2001 |
Keywords
- Bytecode verification
- Data flow analysis
- Java
- Theorem proving