src/HOL/MicroJava/document/root.bib
 author haftmann Tue Nov 24 14:37:23 2009 +0100 (2009-11-24) changeset 33954 1bc3b688548c parent 13067 a59af3a83c61 child 68649 f849fc1cb65e permissions -rwxr-xr-x
backported parts of abstract byte code verifier from AFP/Jinja
     1 @inproceedings{NipkowOP00,

     2         author={Tobias Nipkow and Oheimb, David von and Cornelia Pusch},

     3         title={{$\mu$Java}: Embedding a Programming Language in a Theorem Prover},

     4         booktitle = {Foundations of Secure Computation},

     5         series= {NATO Science Series F: Computer and Systems Sciences},

     6         volume = {175},

     7         year = {2000},

     8         publisher = {IOS Press},

     9         editor = {Friedrich L. Bauer and Ralf Steinbr{\"u}ggen},

    10         abstract = {This paper introduces the subset $micro$Java of Java,

    11 essentially by omitting everything but classes.

    12 The type system and semantics of this language

    13 (and a corresponding abstract Machine $micro$JVM)

    14 are formalized in the theorem prover Isabelle/HOL.

    15 Type safety both of $micro$Java and the $micro$JVM

    16 are mechanically verified.

    17

    18 To make the paper self-contained, it starts with

    19 introductions to Isabelle/HOL and the art of

    20 embedding languages in theorem provers.},

    21         CRClassification = {D.3.1, F.3.2},

    22         CRGenTerms = {Languages, Reliability, Theory, Verification},

    23         url = {\url{http://isabelle.in.tum.de/Bali/papers/MOD99.html}},

    24         pages = {117--144}

    25 }

    26

    27

    28

    29 @inproceedings{DvO-ECOOP00,

    30         author = {David von Oheimb},

    31         title = {Axiomatic Semantics for {J}ava$^{\ell{}ight}$ in {Isabelle/HOL}},

    32         booktitle = {Formal Techniques for {J}ava Programs},

    33         year = {2000},

    34         publisher = {Fernuniversit{{\"a}t} Hagen},

    35         editor = {Drossopoulou, S. and Eisenbach, S. and Jacobs, B. and Leavens, G. T. and M{\"u}ller, P. and Poetzsch-Heffter, A.},

    36         organization = {Technical Report 269, 5/2000},

    37         note = {ECOOP2000 Workshop proceedings available from \url{http://www.informatik.fernuni-hagen.de/pi5/publications.html}},

    38         abstract = {We introduce a Hoare-style calculus for a nearly

    39 full subset of sequential Java, which we call Java_light. In particular,

    40 we present solutions to challenging features like exception handling,

    41 static initialization of classes and dynamic binding of methods.

    42

    43 This axiomatic semantics has been proved sound and complete w.r.t.

    44 our operational semantics of Java_light, described in earlier papers.

    45 To our knowledge, our Hoare logic is the first one for an

    46 object-oriented language that has been proved complete.

    47 The proofs also give new insights into the role of type-safety.

    48

    49 All the formalization and proofs have been done with the

    50 theorem prover Isabelle/HOL.},

    51         CRClassification = {D.2.4, D.3.1, F.3.1},

    52         CRGenTerms = {Languages, Verification, Theory},

    53         url       = {\url{http://isabelle.in.tum.de/Bali/papers/ECOOP00.html}}

    54 }

    55

    56

    57

    58 @inproceedings{KleinN00,

    59 author={Gerwin Klein and Tobias Nipkow},

    60 title={Verified Lightweight Bytecode Verification},

    61         booktitle = {Formal Techniques for {J}ava Programs},

    62         year = {2000},

    63         publisher = {Fernuniversit{{\"a}t} Hagen},

    64         editor = {Drossopoulou, S. and Eisenbach, S. and Jacobs, B. and Leavens, G. T. and M{\"u}ller, P. and Poetzsch-Heffter, A.},

    65         organization = {Technical Report 269, 5/2000},

    66         note = {ECOOP2000 Workshop proceedings available from \url{http://www.informatik.fernuni-hagen.de/pi5/publications.html}},

    67         url       = {\url{http://www4.in.tum.de/~nipkow/pubs/lbv.html}}

    68 }

    69

    70

    71 @article{KleinN-CPE01,

    72         author = "Gerwin Klein and Tobias Nipow",

    73         title = "Verified Lightweight Bytecode Verification",

    74         journal = "Concurrency and Computation: Practice and Experience",

    75         year = "2001",

    76         volume = "13",

    77         number = "13",

    78         editor = "Gary T. Leavens and Susan Eisenbach",

    79         pages = "1133-1151",

    80         url = {http://www4.informatik.tu-muenchen.de/~kleing/papers/cpe01.html},

    81         abstract = {Eva and Kristoffer Rose proposed a (sparse) annotation of Java Virtual

    82 Machine code with types to enable a one-pass verification of welltypedness.

    83 We have formalized a variant of their proposal in the theorem prover

    84 Isabelle/HOL and proved soundness and completeness.},

    85         note = {Invited contribution to special issue on Formal Techniques for Java},

    86 }

    87

    88

    89 @inproceedings{Nipkow-FOSSACS01,author={Tobias Nipkow},

    90 title={Verified Bytecode Verifiers},booktitle=

    91 {Foundations of Software Science and Computation Structures (FOSSACS 2001)},

    92 editor={F. Honsell},publisher=Springer,series=LNCS,volume=2030,

    93 pages={347--363},year=2001}