Premium
Verified lightweight bytecode verification
Author(s) -
Klein Gerwin,
Nipkow Tobias
Publication year - 2001
Publication title -
concurrency and computation: practice and experience
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.309
H-Index - 67
eISSN - 1532-0634
pISSN - 1532-0626
DOI - 10.1002/cpe.597
Subject(s) - soundness , bytecode , hol , programming language , computer science , completeness (order theory) , java , automated theorem proving , java bytecode , gas meter prover , theoretical computer science , mathematical proof , java applet , mathematics , java annotation , mathematical analysis , geometry
Eva and Kristoffer Rose proposed a (sparse) annotation of Java Virtual Machine code with types to enable a one‐pass verification of well‐typedness. We have formalized a variant of their proposal in the theorem prover Isabelle/HOL and proved soundness and completeness. Copyright © 2001 John Wiley & Sons, Ltd.