summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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.

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 }

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.

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.

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 }

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 }

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 }

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}