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}