Java Bytecode Verification for @NonNull Types

Chris Male; David J. Pearce; Alex Potanin; Constantine Dymnikov

doi:10.1007/978-3-540-78791-4_16

Java Bytecode Verification for @NonNull Types

Chris Male^*, David J. Pearce, Alex Potanin, Constantine Dymnikov

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › peer-review

18 Citations (Scopus)

Abstract

Java's annotation mechanism allows us to extend its type system with non-null types. However, checking such types cannot be done using the existing bytecode verification algorithm. We extend this algorithm to verify non-null types using a novel technique that identifies aliasing relationships between local variables and stack locations in the JVM. We formalise this for a subset of Java Bytecode and report on experiences using our implementation.

Original language	English
Title of host publication	Compiler Construction - 17th International Conference, CC 2008 - Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Proceedings
Editors	Laurie Hendren
Place of Publication	Berlin
Publisher	Springer
Pages	229-244
Number of pages	16
ISBN (Electronic)	978-3-540-78791-4
ISBN (Print)	3540787909, 978-3-540-78790-7
DOIs	https://doi.org/10.1007/978-3-540-78791-4_16
Publication status	Published - 2008
Externally published	Yes
Event	17th International Conference on Compiler Construction, CC 2008 - Budapest, Hungary Duration: 29 Mar 2008 → 6 Apr 2008

Publication series

Name	Lecture Notes in Computer Science
Volume	4959 (LNTCS)
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	17th International Conference on Compiler Construction, CC 2008
Country/Territory	Hungary
City	Budapest
Period	29/03/08 → 6/04/08

Access to Document

10.1007/978-3-540-78791-4_16

Cite this

Male, C., Pearce, D. J., Potanin, A., & Dymnikov, C. (2008). Java Bytecode Verification for @NonNull Types. In L. Hendren (Ed.), Compiler Construction - 17th International Conference, CC 2008 - Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Proceedings (pp. 229-244). (Lecture Notes in Computer Science; Vol. 4959 (LNTCS)). Springer. https://doi.org/10.1007/978-3-540-78791-4_16

Male, Chris ; Pearce, David J. ; Potanin, Alex et al. / Java Bytecode Verification for @NonNull Types. Compiler Construction - 17th International Conference, CC 2008 - Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Proceedings. editor / Laurie Hendren. Berlin : Springer, 2008. pp. 229-244 (Lecture Notes in Computer Science).

@inproceedings{2ecc189b45184920a03bc959d0f9df02,

title = "Java Bytecode Verification for @NonNull Types",

abstract = "Java's annotation mechanism allows us to extend its type system with non-null types. However, checking such types cannot be done using the existing bytecode verification algorithm. We extend this algorithm to verify non-null types using a novel technique that identifies aliasing relationships between local variables and stack locations in the JVM. We formalise this for a subset of Java Bytecode and report on experiences using our implementation.",

author = "Chris Male and Pearce, \{David J.\} and Alex Potanin and Constantine Dymnikov",

year = "2008",

doi = "10.1007/978-3-540-78791-4\_16",

language = "English",

isbn = "3540787909",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "229--244",

editor = "Laurie Hendren",

booktitle = "Compiler Construction - 17th International Conference, CC 2008 - Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Proceedings",

address = "Germany",

note = "17th International Conference on Compiler Construction, CC 2008 ; Conference date: 29-03-2008 Through 06-04-2008",

}

Male, C, Pearce, DJ, Potanin, A & Dymnikov, C 2008, Java Bytecode Verification for @NonNull Types. in L Hendren (ed.), Compiler Construction - 17th International Conference, CC 2008 - Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Proceedings. Lecture Notes in Computer Science, vol. 4959 (LNTCS), Springer, Berlin, pp. 229-244, 17th International Conference on Compiler Construction, CC 2008, Budapest, Hungary, 29/03/08. https://doi.org/10.1007/978-3-540-78791-4_16

Java Bytecode Verification for @NonNull Types. / Male, Chris; Pearce, David J.; Potanin, Alex et al.
Compiler Construction - 17th International Conference, CC 2008 - Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Proceedings. ed. / Laurie Hendren. Berlin: Springer, 2008. p. 229-244 (Lecture Notes in Computer Science; Vol. 4959 (LNTCS)).

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › peer-review

TY - GEN

T1 - Java Bytecode Verification for @NonNull Types

AU - Male, Chris

AU - Pearce, David J.

AU - Potanin, Alex

AU - Dymnikov, Constantine

PY - 2008

Y1 - 2008

N2 - Java's annotation mechanism allows us to extend its type system with non-null types. However, checking such types cannot be done using the existing bytecode verification algorithm. We extend this algorithm to verify non-null types using a novel technique that identifies aliasing relationships between local variables and stack locations in the JVM. We formalise this for a subset of Java Bytecode and report on experiences using our implementation.

AB - Java's annotation mechanism allows us to extend its type system with non-null types. However, checking such types cannot be done using the existing bytecode verification algorithm. We extend this algorithm to verify non-null types using a novel technique that identifies aliasing relationships between local variables and stack locations in the JVM. We formalise this for a subset of Java Bytecode and report on experiences using our implementation.

UR - https://www.scopus.com/pages/publications/47249110938

U2 - 10.1007/978-3-540-78791-4_16

DO - 10.1007/978-3-540-78791-4_16

M3 - Conference Paper

AN - SCOPUS:47249110938

SN - 3540787909

SN - 978-3-540-78790-7

T3 - Lecture Notes in Computer Science

SP - 229

EP - 244

BT - Compiler Construction - 17th International Conference, CC 2008 - Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Proceedings

A2 - Hendren, Laurie

PB - Springer

CY - Berlin

T2 - 17th International Conference on Compiler Construction, CC 2008

Y2 - 29 March 2008 through 6 April 2008

ER -

Male C, Pearce DJ, Potanin A, Dymnikov C. Java Bytecode Verification for @NonNull Types. In Hendren L, editor, Compiler Construction - 17th International Conference, CC 2008 - Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Proceedings. Berlin: Springer. 2008. p. 229-244. (Lecture Notes in Computer Science). doi: 10.1007/978-3-540-78791-4_16

Java Bytecode Verification for @NonNull Types

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this