1%----------------------------------------------------------------------
2
3
4@string{AI="Acta Informatica"}
5@string{AP="Academic Press"}
6@string{CACM="Communications of the ACM"}
7@string{CUP="Cambridge University Press"}
8@string{FAC="Formal Aspects of Computing"}
9@string{IC="Information and Computation"}
10@string{IPL="Information Processing Letters"}
11@string{JAR="J. Automated Reasoning"}
12@string{JCSS="J. Computer and System Sciences"}
13@string{JFP="J. Functional Programming"}
14@string{JSC="J. Symbolic Computation"}
15@string{JSL="J. Symbolic Logic"}
16@string{LNCS="Lect.\ Notes in Comp.\ Sci."}
17%@string{LNCS="LNCS"}
18@string{LNAI="Lect.\ Notes in Art.\ Int."}
19@string{OUP="Oxford University Press"}
20@string{MIT="MIT Press"}
21@string{PH="Prentice-Hall"}
22@string{SCP="Science of Computer Programming"}
23@string{Springer="Springer-Verlag"}
24%@string{Springer="Springer"}
25@string{TCS="Theoretical Computer Science"}
26@string{TOPLAS="ACM Trans.\ Programming Languages and Systems"}
27
28@inproceedings{Ballarin-04-locales,
29  author = "Clemens Ballarin",
30  title = "Locales and Locale Expressions in {I}sabelle/{I}sar",
31  pages = "34-50",
32  crossref = "BerardiEtAl2004"
33}
34
35@proceedings{BerardiEtAl2004,
36  editor = "Stefano Berardi and  Mario Coppo and Ferruccio Damiani",
37  title = "{T}ypes for Proofs and Programs: International Workshop,
38{TYPES} 2003, {Torino, Italy, April 30--May 4, 2003}, Selected Papers",
39  booktitle = "Types for Proofs and Programs: International Workshop,
40{TYPES} 2003, {Torino, Italy, April 30--May 4, 2003}, Selected Papers",
41  publisher = Springer,
42  series = LNCS,
43  number = "3085",
44  year = 2004
45}
46
47@Book{Nipkow-02-hol,
48 author={Tobias Nipkow and Lawrence Paulson and Markus Wenzel},
49title="Isabelle/HOL --- A Proof Assistant for Higher-Order Logic",
50publisher=Springer,series=LNCS,volume=2283,year=2002,
51note={\url{http://www.in.tum.de/~nipkow/LNCS2283/}}}
52
53@InProceedings{NaraschewskiW-TPHOLs98,
54author={Wolfgang Naraschewski and Markus Wenzel},
55title=
56{{O}bject-Oriented Verification based on Record Subtyping in Higher-Order Logic},
57booktitle={Theorem Proving in Higher Order Logics:
5811th International Conference, TPHOLs'98},
59publisher=Springer,volume=1479,series=LNCS,year=1998}
60
61@inproceedings{MehtaN-CADE03,author={Farhad Mehta and Tobias Nipkow},
62title={Proving Pointer Programs in Higher-Order Logic},
63booktitle="Automated Deduction --- CADE-19",editor="F. Baader",
64year=2003,publisher=Springer,series=LNCS,volume={2741},pages={121--135}}
65
66@phdthesis{Homeier-95-vcg,
67  author = {Peter V. Homeier},
68  title  = {Trustworthy Tools for Trustworthy Programs: A Mechanically Verified Verification Condition Generator for the Total Correctness of Procedures},
69  school = {Department of Computer Science, University of California, Los Angeles},
70  year = {1995},
71}
72
73@PhdThesis{Schirmer-PhD,
74  author = 	 {Norbert Schirmer},
75  title = 	 {Verification of Sequential Imperative Programs in {I}sabelle/{HOL}},
76  school = 	 {Technische Universit\"at M\"unchen},
77  year = 	 {2006},
78  note = {Available from \url{http://mediatum2.ub.tum.de/doc/601799/601799.pdf}}
79}
80
81@inproceedings{Ortner-Schirmer-TPHOL05,
82author={Veronika Ortner and Norbert Schirmer},
83title={Verification of {BDD} Normalization},
84pages={261--277},
85crossref={TPHOL05}
86}
87
88
89
90@Proceedings{TPHOL05,
91  editor={J. Hurd and T. Melham},
92  title={Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 2005},
93 booktitle={Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 2005},
94  publisher=Springer,
95  series=LNCS,
96  volume=3603,
97  year=2005,
98}
99
100@inproceedings{Leinenbach:SSV08-??,
101AUTHOR = {Leinenbach, D. and Petrova, E.},
102TITLE = {Pervasive Compiler Verification -- From Verified Programs to Verified Systems},
103YEAR = {2008},
104BOOKTITLE = {3rd intl Workshop on Systems Software Verification (SSV08), to appear},
105PUBLISHER = {Elsevier Science B. V.},
106}
107
108@inproceedings{Alkassar:TACAS08-??,
109AUTHOR = {Alkassar, E. and Schirmer, N. and Starostin, A.},
110TITLE = {Formal Pervasive Verification of a Paging Mechanism},
111YEAR = {2008},
112SERIES = {LNCS},
113BOOKTITLE = {14th intl Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS08), to appear},
114PUBLISHER = {Springer},
115}
116
117@inproceedings{Tuch:separation-logic:2007,
118  author = {Harvey Tuch and Gerwin Klein and Michael Norrish},
119  title = {Types, Bytes, and Separation Logic},
120  booktitle = {POPL '07: Proceedings of the 34th annual ACM SIGPLAN-SIGACT
121               symposium on Principles of programming languages},
122  year = 2007,
123  isbn = {1-59593-575-4},
124  pages = {97--108},
125  location = {Nice, France},
126  doi = {http://doi.acm.org/10.1145/1190216.1190234},
127  publisher = {ACM Press},
128  address = {New York, NY, USA},
129}