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

src/HOL/NanoJava/document/root.bib

author | wenzelm |

Sun Sep 18 20:33:48 2016 +0200 (2016-09-18) | |

changeset 63915 | bab633745c7f |

parent 11565 | ab004c0ecc63 |

child 68649 | f849fc1cb65e |

permissions | -rw-r--r-- |

tuned proofs;

1 @misc{NanoJava,

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

3 title={Hoare Logic for {NanoJava}: Auxiliary Variables,

4 Side Effects and Virtual Methods revisited},

5 year = {2002},

6 abstract = {We give a Hoare logic for NanoJava,

7 a small fragment of Java with essentially just classes.

8 The logic is proved sound and (relatively) complete within Isabelle/HOL.

9 We introduce an elegant new approach for expressing auxiliary variables:

10 by universal quantification on the outer logical level.

11 Furthermore, we give simple means of handling side-effecting expressions

12 and dynamic binding within method calls.},

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

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

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

16 note = {Submitted for publication.}

17 }

19 @inproceedings{NipkowOP00,

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

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

22 booktitle = {Foundations of Secure Computation},

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

24 volume = {175},

25 year = {2000},

26 publisher = {IOS Press},

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

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

29 essentially by omitting everything but classes.

30 The type system and semantics of this language

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

32 are formalized in the theorem prover Isabelle/HOL.

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

34 are mechanically verified.

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

37 introductions to Isabelle/HOL and the art of

38 embedding languages in theorem provers.},

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

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

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

42 pages = {117--144}

43 }

46 @article{DvO-CPE01,

47 author = {David von Oheimb},

48 title = {Hoare Logic for {J}ava in {Isabelle/HOL}},

49 journal = {Concurrency: Practice and Experience},

50 year = {2001},

51 volume = 598,

52 pages = {??--??+43},

53 url = {http://www4.in.tum.de/papers/DvO-CPE01.html},

54 abstract = {

55 This article presents a Hoare-style calculus for a substantial subset

56 of Java Card, which we call Java_light. In particular, the language

57 includes side-effecting expressions, mutual recursion, dynamic method

58 binding, full exception handling, and static class initialization.

60 The Hoare logic of partial correctness is proved not only sound (w.r.t.

61 our operational semantics of Java_light, described in detail elsewhere)

62 but even complete. It is the first logic for an object-oriented

63 language that is provably complete.

64 The completeness proof uses a refinement of the Most General Formula

65 approach. The proof of soundness gives new insights into the role of

66 type safety. Further by-products of this work are a new general

67 methodology for handling side-effecting expressions and their results,

68 the discovery of the strongest possible rule of consequence, and a

69 flexible Call rule for mutual recursion.

70 We also give a small but non-trivial application example.

72 All definitions and proofs have been done formally with the interactive

73 theorem prover Isabelle/HOL. This guarantees not only rigorous definitions,

74 but also gives maximal confidence in the results obtained.},

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

76 CRGenTerms = {Languages, Verification, Theory},

77 note = {\url{http://isabelle.in.tum.de/Bali/papers/CPE01.html}, to appear}

78 }