9931
|
1 |
@inproceedings{NipkowOP00,
|
9986
|
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},
|
9988
|
5 |
series= {NATO Science Series F: Computer and Systems Sciences},
|
9986
|
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},
|
9988
|
31 |
title = {Axiomatic Semantics for {J}ava$^{\ell{}ight}$ in {Isabelle/HOL}},
|
9986
|
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.},
|
10027
|
36 |
organization = {Technical Report 269, 5/2000},
|
9988
|
37 |
note = {ECOOP2000 Workshop proceedings available from \url{http://www.informatik.fernuni-hagen.de/pi5/publications.html}},
|
9986
|
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.},
|
10027
|
65 |
organization = {Technical Report 269, 5/2000},
|
9988
|
66 |
note = {ECOOP2000 Workshop proceedings available from \url{http://www.informatik.fernuni-hagen.de/pi5/publications.html}},
|
9986
|
67 |
url = {\url{http://www4.in.tum.de/~nipkow/pubs/lbv.html}}
|
|
68 |
}
|
13067
|
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}
|