JVM Bytecode Verification Without Dataflow Analysis
Ian Bayley, Sam Shiel · Electronic Notes in Theoretical Computer Science · 2005
Bytecode verification algorithms are traditionally based on dataflow analysis. We present an alternative algorithm that first restructures the bytecode and then infers a type signature for each method in a manner typical of functional programming languages. We also give an operational semantics to an algebra of structured bytecode and thereby prove both that restructuring preserves semantics and that our type inference is sound.