Skip to main content
Conference ProceedingsOPEN ACCESS

Verified bytecode verifiers

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (2001) 2030 347-363
DOI: 10.1007/3-540-45315-6_23
27Citations
Citations of this article
13Readers
Mendeley users who have this article in their library.

This article is free to access.

Abstract

Using the theorem prover Isabelle/HOL we have formalized and proved correct an executable bytecode verifier in the style of Kildall’s algorithm for a significant subset of the Java Virtual Machine. First an abstract framework for proving correctness of data flow based type inference algorithms for assembly languages is formalized. It is shown that under certain conditions Kildall’s algorithm yields a correct bytecode verifier. Then the framework is instantiated with a model of the JVM.

Cite

CITATION STYLE

APA

Nipkow, T. (2001). Verified bytecode verifiers. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2030, pp. 347–363). Springer Verlag. https://doi.org/10.1007/3-540-45315-6_23

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free