article · 1998

Java Bytecode Verification Using Model Checking

Joachim Posegga, Harald Vogt

Cited by 0Abstract and details only

Abstract

We provide an abstract interpretation for Java bytecode programs to build finite state models of these programs. We describe the bytecode constraints as CTL formulas which can be checked against the finite models by a (standard) model checker. We see a practical way to perform bytecode verification on a formal basis in that it could help to achieve higher security and open the door for further extensions to prove additional properties of Java bytecode.

Cite this paper

APA 7

Posegga, J., & Vogt, H. (1998). Java Bytecode Verification Using Model Checking.

MLA 9

Posegga, Joachim, and Harald Vogt. “Java Bytecode Verification Using Model Checking.” 1998.

Chicago

Posegga, Joachim, and Harald Vogt. 1998. “Java Bytecode Verification Using Model Checking.”

Harvard

Posegga, J. and Vogt, H. (1998) ‘Java Bytecode Verification Using Model Checking’.

BibTeX

@article{posegga1998java,
  title = {{Java Bytecode Verification Using Model Checking}},
  author = {Posegga, Joachim and Vogt, Harald},
  year = {1998}
}

Made from the index record. Check names, capitalisation and page numbers against the paper. Need another style? AI for Research has over 10,000.