scholarly journals Generating Verification Conditions from BIRS Code using Basic Paths for Java Bytecode Verification

2012 ◽  
Vol 17 (8) ◽  
pp. 61-69
Author(s):  
Je-Min Kim ◽  
Seon-Tae Kim ◽  
Joon-Seok Park ◽  
Weon-Hee Yoo
Keyword(s):  
Bytecode Verification ◽  
Java Bytecode ◽  
Verification Conditions

scholarly journals Integrated Java Bytecode Verification

2005 ◽  
Vol 131 ◽  
pp. 27-38 ◽  
Author(s):  
Andreas Gal ◽  
Christian W. Probst ◽  
Michael Franz
Keyword(s):  
Bytecode Verification ◽  
Java Bytecode

Adaptiveness in well-typed Java bytecode verification

2006 ◽  
Author(s):  
F. Y. Huang ◽  
C. B. Jay ◽  
D. B. Skillicorn
Keyword(s):  
Bytecode Verification ◽  
Java Bytecode

scholarly journals Java Bytecode Verification for @NonNull Types

2008 ◽  
pp. 229-244 ◽  
Author(s):  
Chris Male ◽  
David J. Pearce ◽  
Alex Potanin ◽  
Constantine Dymnikov
Keyword(s):  
Bytecode Verification ◽  
Java Bytecode

scholarly journals Java Bytecode Verification with OCL Why, How and Whenc.

2020 ◽  
Vol 19 (3) ◽  
pp. 3:1
Author(s):  
Christoph Bockisch ◽  
Gabriele Taentzer ◽  
Nebras Nassar ◽  
Lukas Wydra
Keyword(s):  
Bytecode Verification ◽  
Java Bytecode

Verified Java Bytecode Verification (Verified Java Bytecode Verification)

2005 ◽  
Vol 47 (2) ◽  
Author(s):  
Gerwin Klein
Keyword(s):  
Bytecode Verification ◽  
Eingebettete Systeme ◽  
Java Bytecode

ZusammenfassungDer Bytecode Verifier ist ein essenzieller Bestandteil der Sicherheitsarchitektur der Programmierplattform Java. Die vorliegende Dissertation stellt eine formale, ausführbare Spezifikation des Bytecode Verifiers vor sowie den Beweis, dass diese korrekt ist. Die Formalisierung, vollständig im Theorembeweiser Isabelle durchgeführt, besteht aus einem abstrakten Framework für Bytecode-Verifikation, das mit zunehmend ausdrucksstarken Typsystemen instanziiert wird. Diese decken sämtliche wichtigen Eigenschaften der Java-Plattform ab. Die Formalisierung liefert zwei ausführbare, verifizierte Bytecode Verifier: den Standard-Algorithmus, wie er auf normalen Desktop-Rechnern benutzt wird, und einen Lightweight Bytecode Verifier für eingebettete Systeme mit Ressourcenbeschränkungen wie z.B. Java SmartCards.

scholarly journals Using abstract interpretation to add type checking for interfaces in Java bytecode verification

2010 ◽  
Vol 411 (22-24) ◽  
pp. 2174-2201 ◽  
Author(s):  
Nicoletta De Francesco ◽  
Giuseppe Lettieri ◽  
Luca Martini
Keyword(s):  
Abstract Interpretation ◽  
Type Checking ◽  
Bytecode Verification ◽  
Java Bytecode

scholarly journals Java Bytecode Verification by Model Checking

1999 ◽  
pp. 491-494 ◽  
Author(s):  
David Basin ◽  
Stefan Friedrich ◽  
Joachim Posegga ◽  
Harald Vogt
Keyword(s):  
Model Checking ◽  
Bytecode Verification ◽  
Java Bytecode
Sign in / Sign up

Export Citation Format

Share Document