% BibTeX bibliography file


@techreport{jovial:pv,
	TITLE = {A {JOVIAL} Verifier},
	AUTHOR = {B. Elspas and M. Green and M. Moriconi and R. Shostak},
	MONTH = jan,
	YEAR = 1979,
	INSTITUTION = {Computer Science Laboratory, SRI International}
}

@article{Robinson&Levitt,
	TITLE = {Proof Techniques for Hierarchically Structured Programs},
	AUTHOR = {Lawrence Robinson and Karl N. Levitt},
	JOURNAL = {Communications of the ACM},
	PAGES = {271--283},
	VOLUME = 20,
	NUMBER = 4,
	MONTH = apr,
	YEAR = 1976
}

@manual{HDM:Handbook,
	TITLE = {The {HDM} Handbook},
	AUTHOR = {L. Robinson and K. N. Levitt and B. A. Silverberg},
	MONTH = jun,
	YEAR = 1979,
	ORGANIZATION = {Computer Science Laboratory, SRI International},
	ADDRESS = {Menlo Park, CA},
	NOTE = {Three Volumes}
}

@article{Spitzen:example,
	TITLE = {An Example of Hierarchical Design and Proof},
	AUTHOR = {Jay M. Spitzen and Karl N. Levitt and Lawrence Robinson},
	JOURNAL = {Communications of the ACM},
	PAGES = {1064--1075},
	VOLUME = 21,
	NUMBER = 12,
	MONTH = dec,
	YEAR = 1978
}

@techreport{Feiertag:Tool,
	TITLE = {A Technique for Proving Specifications are Multilevel
		Secure},
	AUTHOR = {R. J. Feiertag},
	NUMBER = {CSL-109},
	MONTH = jan,
	YEAR = 1980,
	INSTITUTION = {Computer Science Laboratory, SRI International},
	ADDRESS = {Menlo Park, CA}
}

@inproceedings{FLR77,
	TITLE = {Proving Multilevel Security of a System Design},
	AUTHOR = {R. J. Feiertag and K. N. Levitt and L. Robinson},
	BOOKTITLE = {Sixth ACM Symposium on Operating System Principles},
	PAGES = {57--65},
	MONTH = nov,
	YEAR = 1977
}

@inproceedings{Benzel:scomp-eval,
	TITLE = {Analysis of a Kernel Verification},
	AUTHOR = {Terry Vickers Benzel},
	BOOKTITLE = {Proceedings of the Symposium on Security and Privacy},
	PAGES = {125--131},
	MONTH = apr,
	YEAR = 1984,
	ORGANIZATION = {IEEE Computer Society},
	ADDRESS = {Oakland, CA}
}

@inproceedings{Silverman83,
	TITLE = {Reflections on the Verification of the Security of an
		Operating System Kernel},
	AUTHOR = {J. M. Silverman},
	BOOKTITLE = {Ninth ACM Symposium on Operating System Principles},
	PAGES = {143--154},
	MONTH = oct,
	YEAR = 1983,
	ADDRESS = {Bretton Woods, NH},
	NOTE = {(ACM Operating Systems Review, Vol.\ 17, No.\ 5)}
}

@manual{Criteria,
	TITLE = {Department of Defense Trusted Computer System Evaluation
		Criteria},
	MONTH = dec,
	YEAR = 1985,
	ORGANIZATION = {Department of Defense},
	NOTE = {DOD 5200.28-STD (supersedes CSC-STD-001-83)}
}

@inproceedings{Lindsay88:Regency,
	TITLE = {A Taxonomy of the Causes of Proof Failures in Applications
		Using the {HDM} Methodology},
	AUTHOR = {Kenneth S. Lindsay},
	BOOKTITLE = {Fourth Aerospace Computer Security Applications
		Conference},
	PAGES = {419--423},
	MONTH = dec,
	YEAR = 1988,
	ORGANIZATION = {IEEE Computer Society},
	ADDRESS = {Orlando, FL},
	NOTE = {Reprinted in~\cite[pp.~79--83]{Compass89}}
}

@inproceedings{Regency88,
	TITLE = {A Description of a Formal Verification and Validation
		{(FVV)} Process},
	AUTHOR = {Bill Smith and Cynthia Reese and Kenneth S. Lindsay
		and Brian Crane},
	BOOKTITLE = {Fourth Aerospace Computer Security Applications
		Conference},
	PAGES = {401--408},
	MONTH = dec,
	YEAR = 1988,
	ORGANIZATION = {IEEE Computer Society},
	ADDRESS = {Orlando, FL},
	NOTE = {Reprinted in~\cite[pp.~71--78]{Compass89}}
}

@book{Boyer-Moore79,
	TITLE = {A Computational Logic},
	AUTHOR = {R. S. Boyer and J S. Moore},
	PUBLISHER = {Academic Press},
	YEAR = 1979,
	ADDRESS = {New York, NY}
}

@inproceedings{STP,
	TITLE = {{STP}: A Mechanized Logic for Specification and Verification},
	AUTHOR = {R. E. Shostak and R. Schwartz and P. M. Melliar-Smith},
	BOOKTITLE = {6th International Conference on Automated Deduction
		(CADE)},
	EDITOR = {D. Loveland},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 138,
	YEAR = 1982,
	ADDRESS = {New York, NY}
}

@article{Shostak:sup-inf,
	TITLE = {On the {SUP-INF} Method for Proving {Presburger} Formulas},
	AUTHOR = {Robert E. Shostak},
	JOURNAL = {Journal of the ACM},
	PAGES = {529--543},
	VOLUME = 24,
	NUMBER = 4,
	MONTH = oct,
	YEAR = 1977
}

@article{Shostak:equality,
	TITLE = {An Algorithm for Reasoning about Equality},
	AUTHOR = {Robert E. Shostak},
	JOURNAL = {Communications of the ACM},
	PAGES = {583--585},
	VOLUME = 21,
	NUMBER = 7,
	MONTH = jul,
	YEAR = 1978
}

@article{Shostak:arithmetic,
	TITLE = {A Practical Decision Procedure for Arithmetic with Function
		Symbols},
	AUTHOR = {Robert E. Shostak},
	JOURNAL = {Journal of the ACM},
	PAGES = {351--360},
	VOLUME = 26,
	NUMBER = 2,
	MONTH = apr,
	YEAR = 1979
}

@article{Shostak:residues,
	TITLE = {Deciding Linear Inequalities by Computing Loop Residues},
	AUTHOR = {Robert E. Shostak},
	JOURNAL = {Journal of the ACM},
	PAGES = {769--779},
	VOLUME = 28,
	NUMBER = 4,
	MONTH = oct,
	YEAR = 1981
}

@article{Shostak:combination,
	TITLE = {Deciding Combinations of Theories},
	AUTHOR = {Robert E. Shostak},
	JOURNAL = {Journal of the ACM},
	PAGES = {1--12},
	VOLUME = 31,
	NUMBER = 1,
	MONTH = jan,
	YEAR = 1984
}

@inproceedings{Weinstock80,
	TITLE = {{SIFT}: System Design and Implementation},
	AUTHOR = {Charles B. Weinstock},
	BOOKTITLE = {Fault Tolerant Computing Symposium 10},
	PAGES = {75--77},
	MONTH = oct,
	YEAR = 1980,
	ORGANIZATION = {IEEE Computer Society},
	ADDRESS = {Kyoto, Japan},
	NOTE = {Reprinted in~\cite[pp.\ 29--30]{FTCS-highlights}}
}

@article{SIFT-design,
	TITLE = {{SIFT}: Design and Analysis of a Fault-Tolerant Computer
		for Aircraft Control},
	AUTHOR = {John H. Wensley and Leslie Lamport and Jack Goldberg
		and Milton W. Green and Karl N. Levitt and P. M. Melliar-Smith
		and Robert E. Shostak and Charles B. Weinstock},
	JOURNAL = {Proceedings of the IEEE},
	PAGES = {1240--1255},
	VOLUME = 66,
	NUMBER = 10,
	MONTH = oct,
	YEAR = 1978
}

@article{Sift-verif,
	TITLE = {Formal Specification and Verification of {SIFT}: A Fault-Tolerant
		Flight Control System},
	AUTHOR = {P. M. Melliar-Smith and R. L. Schwartz},
	JOURNAL = {IEEE Transactions on Computers},
	PAGES = {616--630},
	VOLUME = {C-31},
	NUMBER = 7,
	MONTH = jul,
	YEAR = 1982
}

@proceedings{SIFT:review,
	TITLE = {Peer Review of a Formal Verification/Design Proof Methodology},
	MONTH = jul,
	YEAR = 1983,
	ORGANIZATION = {NASA Conference Publication 2377}
}

@incollection{Shostak:circuits,
	TITLE = {Formal Verification of Circuit Designs},
	AUTHOR = {Robert E. Shostak},
	BOOKTITLE = {Computer Hardware Description Languages},
	EDITOR = {T. Uehara and M. Barbacci},
	PAGES = {13--29},
	PUBLISHER = {North-Holland},
	YEAR = 1983
}

@techreport{Kemmerer:assess,
	TITLE = {Verification Assessment Study Final Report},
	AUTHOR = {Richard A. Kemmerer},
	BOOKTITLE = {Verification Assessment Study Final Report},
	NUMBER = {C3-CR01-86},
	YEAR = 1986,
	INSTITUTION = {National Computer Security Center},
	ADDRESS = {Ft.\ Meade, MD},
	NOTE = {5 Volumes (Overview, Gypsy, Affirm, FDM, and {\sc Ehdm}).
		US distribution only}
}

@inproceedings{Melliar-Smith&Rushby,
	TITLE = {The {Enhanced HDM} System for Specification and Verification},
	AUTHOR = {P. Michael Melliar-Smith and John Rushby},
	BOOKTITLE = {Proc.\ VerkShop III},
	PAGES = {41--43},
	MONTH = feb,
	YEAR = 1985,
	ADDRESS = {Watsonville, CA},
	NOTE = {Published as ACM Software Engineering Notes, Vol.\ 10,
		No.\ 4, Aug.\
 85}
}

@inproceedings{Rushby:HDM,
	TITLE = {The Security Model of {Enhanced HDM}},
	AUTHOR = {John Rushby},
	BOOKTITLE = {Proceedings 7th DoD/NBS Computer Security Initiative
		Conference},
	PAGES = {120--136},
	MONTH = sep,
	YEAR = 1984,
	ADDRESS = {Gaithersburg, MD}
}

@inproceedings{EHDM:Overview88,
	TITLE = {The {{\sc Ehdm}} Verification Environment: An Overview},
	AUTHOR = {F. W. von Henke and J. S. Crow and R. Lee and J. M.
		Rushby and R. A. Whitehurst},
	BOOKTITLE = {Proceedings 11th National Computer Security Conference},
	PAGES = {147--155},
	MONTH = oct,
	YEAR = 1988,
	ORGANIZATION = {NBS/NCSC},
	ADDRESS = {Baltimore, MD}
}

@techreport{EHDM:tutorial,
	TITLE = {An Introduction to Formal Specification and Verification
		Using {{\sc Ehdm}}},
	AUTHOR = {John Rushby and Friedrich von Henke and Sam Owre},
	NUMBER = {SRI-CSL-91-2},
	MONTH = feb,
	YEAR = 1991,
	INSTITUTION = {Computer Science Laboratory, SRI International},
	ADDRESS = {Menlo Park, CA}
}

@inproceedings{DiVito-DCCA-3,
	TITLE = {Formal Techniques for Synchronized Fault-Tolerant Systems},
	AUTHOR = {Ben L. {Di Vito} and Ricky W. Butler},
	BOOKTITLE = {Dependable Computing for Critical Applications---3},
	EDITOR = {C. E. Landwehr and B. Randell and L. Simoncini},
	PAGES = {163--188},
	PUBLISHER = {Springer-Verlag, Vienna, Austria},
	SERIES = {Dependable Computing and Fault-Tolerant Systems},
	VOLUME = 8,
	MONTH = sep,
	YEAR = 1992
}

@techreport{Miner93,
	TITLE = {Verification of Fault-Tolerant Clock Synchronization
		Systems},
	AUTHOR = {Paul S. Miner},
	TYPE = {NASA Technical Paper},
	NUMBER = 3349,
	MONTH = nov,
	YEAR = 1993,
	INSTITUTION = {NASA Langley Research Center},
	ADDRESS = {Hampton, VA}
}

@techreport{Rushby92:OM,
	TITLE = {Formal Verification of an {Oral Messages} Algorithm
		for Interactive Consistency},
	AUTHOR = {John Rushby},
	NUMBER = {SRI-CSL-92-1},
	MONTH = jul,
	YEAR = 1992,
	INSTITUTION = {Computer Science Laboratory, SRI International},
	ADDRESS = {Menlo Park, CA},
	NOTE = {Also available as NASA Contractor Report 189704, October
		1992}
}

@incollection{Rushby93:masking,
	TITLE = {A Fault-Masking and Transient-Recovery Model for Digital
		Flight-Control Systems},
	AUTHOR = {John Rushby},
	BOOKTITLE = {Formal Techniques in Real-Time and Fault-Tolerant
		Systems},
	CHAPTER = 5,
	EDITOR = {Jan Vytopil},
	PAGES = {109--136},
	PUBLISHER = {Kluwer},
	SERIES = {Kluwer International Series in Engineering and Computer
		Science},
	YEAR = 1993,
	ADDRESS = {Boston, Dordecht, London}
}

@inproceedings{Rushby94:icah,
	TITLE = {A Formally Verified Algorithm for Clock Synchronization
		Under a Hybrid Fault Model},
	AUTHOR = {John Rushby},
	BOOKTITLE = {Thirteenth ACM Symposium on Principles of Distributed
		Computing},
	PAGES = {304--313},
	MONTH = aug,
	YEAR = 1994,
	ORGANIZATION = {Association for Computing Machinery},
	ADDRESS = {Los Angeles, CA},
	NOTE = {Also available as NASA Contractor Report 198289}
}

@article{Rushby&vonHenke93,
	TITLE = {Formal Verification of Algorithms for Critical Systems},
	AUTHOR = {John Rushby and Friedrich von Henke},
	JOURNAL = {IEEE Transactions on Software Engineering},
	PAGES = {13--23},
	VOLUME = 19,
	NUMBER = 1,
	MONTH = jan,
	YEAR = 1993
}

@inproceedings{Shankar:clocks:Nijmegen,
	TITLE = {Mechanical Verification of a Generalized Protocol for
		{Byzantine} Fault-Tolerant Clock Synchronization},
	AUTHOR = {Natarajan Shankar},
	BOOKTITLE = {Formal Techniques in Real-Time and Fault-Tolerant
		Systems},
	EDITOR = {J. Vytopil},
	PAGES = {217--236},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 571,
	MONTH = jan,
	YEAR = 1992,
	ADDRESS = {Nijmegen, The Netherlands}
}

@article{Butler-Sjogren91,
	TITLE = {Formal Design Verification of Digital Circuitry},
	AUTHOR = {Ricky W. Butler and Jon A. Sjogren},
	JOURNAL = {Reliability Engineering and System Safety},
	PAGES = {67--93},
	VOLUME = 32,
	YEAR = 1991
}

@inproceedings{Joyce&all:compcon,
	TITLE = {From Formal Verification to Silicon Compilation},
	AUTHOR = {J. Joyce and E. Liu and J. Rushby and N. Shankar and
		R. Suaya and F. von Henke},
	BOOKTITLE = {IEEE Compcon},
	PAGES = {450--455},
	MONTH = feb,
	YEAR = 1991,
	ADDRESS = {San Francisco, CA}
}

@manual{PVS:tutorial,
	TITLE = {PVS Tutorial},
	AUTHOR = {N. Shankar and S. Owre and J. M. Rushby},
	MONTH = feb,
	YEAR = 1993,
	ORGANIZATION = {Computer Science Laboratory, SRI International},
	ADDRESS = {Menlo Park, CA},
	NOTE = {Also appears in Tutorial Notes, {\em Formal Methods Europe
		'93: Industrial-Strength Formal Methods}, pages 357--406,
		Odense, Denmark, April 1993}
}

@inproceedings{PVS96:CAV,
	TITLE = {{PVS}: Combining Specification, Proof Checking, and
		Model Checking},
	AUTHOR = {S. Owre and S. Rajan and J.M. Rushby and N. Shankar
		and M.K. Srivas},
	BOOKTITLE = {Computer-Aided Verification, CAV '96},
	EDITOR = {Rajeev Alur and Thomas A. Henzinger},
	PAGES = {411--414},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1102,
	MONTH = {July/August},
	YEAR = 1996,
	ADDRESS = {New Brunswick, NJ}
}

@inproceedings{PVS-CADE92,
	TITLE = {{PVS}: A Prototype Verification System},
	AUTHOR = {S. Owre and J. M. Rushby and N. Shankar},
	BOOKTITLE = {11th International Conference on Automated Deduction
		(CADE)},
	EDITOR = {Deepak Kapur},
	PAGES = {748--752},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Artificial Intelligence},
	VOLUME = 607,
	MONTH = jun,
	YEAR = 1992,
	ADDRESS = {Saratoga, NY}
}

@inproceedings{Shankar96:FMCAD,
	TITLE = {{PVS}: Combining Specification, Proof Checking, and
		Model Checking},
	AUTHOR = {N. Shankar},
	BOOKTITLE = {Formal Methods in Computer-Aided Design (FMCAD '96)},
	EDITOR = {Mandayam Srivas and Albert Camilleri},
	PAGES = {257--264},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1166,
	MONTH = nov,
	YEAR = 1996,
	ADDRESS = {Palo Alto, CA}
}

@inproceedings{Owre-etal98:FM-TRENDS,
	TITLE = {{PVS:} An Experience Report},
	AUTHOR = {Sam Owre and John Rushby and N. Shankar and David Stringer-Calvert},
	BOOKTITLE = {Applied Formal Methods---FM-Trends 98},
	EDITOR = {Dieter Hutter and Werner Stephan and Paolo Traverso
		and Markus Ullman},
	PAGES = {338--345},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1641,
	MONTH = oct,
	YEAR = 1998,
	ADDRESS = {Boppard, Germany}
}

@manual{PVS:language,
	TITLE = {PVS Language Reference},
	AUTHOR = {S. Owre and N. Shankar and J. M. Rushby and D. W. J.
		Stringer-Calvert},
	MONTH = sep,
	YEAR = 1999,
	ORGANIZATION = {Computer Science Laboratory, SRI International},
	ADDRESS = {Menlo Park, CA}
}

@manual{PVS:prover,
	TITLE = {PVS Prover Guide},
	AUTHOR = {N. Shankar and S. Owre and J. M. Rushby and D. W. J.
		Stringer-Calvert},
	MONTH = sep,
	YEAR = 1999,
	ORGANIZATION = {Computer Science Laboratory, SRI International},
	ADDRESS = {Menlo Park, CA}
}

@manual{PVS:userguide,
	TITLE = {PVS System Guide},
	AUTHOR = {S. Owre and N. Shankar and J. M. Rushby and D. W. J.
		Stringer-Calvert},
	MONTH = sep,
	YEAR = 1999,
	ORGANIZATION = {Computer Science Laboratory, SRI International},
	ADDRESS = {Menlo Park, CA}
}

@techreport{PVS-Semantics:TR,
	TITLE = {The Formal Semantics of {PVS}},
	AUTHOR = {Sam Owre and Natarajan Shankar},
	NUMBER = {SRI-CSL-97-2},
	MONTH = aug,
	YEAR = 1997,
	INSTITUTION = {Computer Science Laboratory, SRI International},
	ADDRESS = {Menlo Park, CA}
}

@article{Owre95:prolegomena,
	TITLE = {Formal Verification for Fault-Tolerant Architectures:
		Prolegomena to the Design of {PVS}},
	AUTHOR = {Sam Owre and John Rushby and Natarajan Shankar and
		Friedrich von Henke},
	JOURNAL = {IEEE Transactions on Software Engineering},
	PAGES = {107--125},
	VOLUME = 21,
	NUMBER = 2,
	MONTH = feb,
	YEAR = 1995
}

@article{Rushby98:TSE,
	TITLE = {Subtypes for Specifications: Predicate Subtyping in
		{PVS}},
	AUTHOR = {John Rushby and Sam Owre and N. Shankar},
	JOURNAL = {IEEE Transactions on Software Engineering},
	PAGES = {709--720},
	VOLUME = 24,
	NUMBER = 9,
	MONTH = sep,
	YEAR = 1998
}

@inproceedings{Shankar&Owre:WADT99,
	TITLE = {Principles and Pragmatics of Subtyping in {PVS}},
	AUTHOR = {Natarajan Shankar and Sam Owre},
	BOOKTITLE = {Recent Trends in Algebraic Development Techniques,
		{WADT '99}},
	EDITOR = {Didier Bert and Christine Choppy and Peter Mosses},
	PAGES = {37--52},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1827,
	MONTH = sep,
	YEAR = 1999,
	ADDRESS = {Toulouse, France}
}

@techreport{Butler:PVS-tut,
	TITLE = {An Elementary Tutorial on Formal Specification and Verification
		Using {PVS 2}},
	AUTHOR = {Ricky W. Butler},
	TYPE = {NASA Technical Memorandum},
	NUMBER = 108991,
	MONTH = jun,
	YEAR = 1993,
	INSTITUTION = {NASA Langley Research Center},
	ADDRESS = {Hampton, VA},
	NOTE = {Revised June 1995. Available, with PVS specification
		files, at \url{http://atb-www.larc.nasa.gov/ftp/larc/PVS-tutorial};
		use only files marked ``revised.''}
}

@misc{WIFT-Tut,
	TITLE = {A Tutorial Introduction to {PVS}},
	AUTHOR = {Judy Crow and Sam Owre and John Rushby and Natarajan
		Shankar and Mandayam Srivas},
	HOWPUBLISHED = {Presented at WIFT '95: Workshop on Industrial-Strength
		Formal Specification Techniques, Boca Raton, Florida},
	MONTH = apr,
	YEAR = 1995,
	INSTITUTION = {Computer Science Laboratory, SRI International},
	ADDRESS = {Menlo Park, CA},
	NOTE = {Available, with specification files, at \url{http://www.csl.sri.com/wift-tutorial.html}}
}

@techreport{Rushby&Stringer-Calvert95,
	TITLE = {A Less Elementary Tutorial for the {PVS} Specification
		and Verification System},
	AUTHOR = {John Rushby and David W. J. Stringer-Calvert},
	NUMBER = {SRI-CSL-95-10},
	MONTH = jun,
	YEAR = 1995,
	INSTITUTION = {Computer Science Laboratory, SRI International},
	ADDRESS = {Menlo Park, CA},
	NOTE = {Revised, July 1996. Available, with specification files,
		at \url{http://www.csl.sri.com/csl-95-10.html}}
}

@inproceedings{Owre94:TPCD,
	TITLE = {A Tutorial on Using {PVS} for Hardware Verification},
	AUTHOR = {S. Owre and J. M. Rushby and N. Shankar and M. K. Srivas},
	BOOKTITLE = {Theorem Provers in Circuit Design ({TPCD} '94)},
	EDITOR = {Ramayya Kumar and Thomas Kropf},
	PAGES = {258--279},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 910,
	MONTH = sep,
	YEAR = 1994,
	ADDRESS = {Bad Herrenalb, Germany}
}

@techreport{PVS-ADT:TR,
	TITLE = {Abstract Datatypes in {PVS}},
	AUTHOR = {Sam Owre and Natarajan Shankar},
	NUMBER = {SRI-CSL-93-9R},
	MONTH = dec,
	YEAR = 1993,
	INSTITUTION = {Computer Science Laboratory, SRI International},
	ADDRESS = {Menlo Park, CA},
	NOTE = {Extensively revised June 1997; Also available as NASA
		Contractor Report CR-97-206264}
}

@techreport{Owre95:tables,
	TITLE = {Analyzing Tabular and State-Transition Specifications
		in {PVS}},
	AUTHOR = {Sam Owre and John Rushby and Natarajan Shankar},
	NUMBER = {SRI-CSL-95-12},
	MONTH = jul,
	YEAR = 1995,
	INSTITUTION = {Computer Science Laboratory, SRI International},
	ADDRESS = {Menlo Park, CA},
	NOTE = {Available, with specification files, at \url{http://www.csl.sri.com/csl-95-12.html}.
		Also published as NASA Contractor Report 201729.}
}

@misc{FORTE97-Tut,
	TITLE = {Specification, Proof Checking, and Model Checking for
		Protocols and Distributed Systems with {PVS}},
	AUTHOR = {John Rushby},
	HOWPUBLISHED = {Tutorial presented at {FORTE X/PSTV XVII '97}:
		Formal Description Techniques and Protocol Specification,
		Testing and Verification},
	MONTH = nov,
	YEAR = 1997,
	INSTITUTION = {Computer Science Laboratory, SRI International},
	ADDRESS = {Menlo Park, CA},
	NOTE = {Available, with specification files, at \url{http://www.csl.sri.com/forte97.html}}
}

@inproceedings{Rushby00:Movep2k,
	TITLE = {Theorem Proving for Verification},
	AUTHOR = {John Rushby},
	BOOKTITLE = {Modelling and Verification of Parallel Processes:
		MoVEP 2k},
	EDITOR = {Franck Cassez},
	MONTH = jun,
	YEAR = 2000,
	ADDRESS = {Nantes, France},
	NOTE = {Tutorial presented at MoVEP: revised version to be published
		by Springer LNCS}
}

@manual{NASA-GB1,
	TITLE = {NASA Formal Methods Specification and Verification Guidebook
		for Software and Computer Systems, Volume I: Planning
		and Technology Insertion},
	AUTHOR = {Judith Crow and others},
	NUMBER = {NASA-GB-002-95},
	YEAR = 1995,
	ORGANIZATION = {NASA Office of Safety and Mission Assurance},
	ADDRESS = {Washington, DC},
	NOTE = {Available at \url{http://eis.jpl.nasa.gov/quality/Formal_Methods/}}
}

@manual{NASA-GB2,
	TITLE = {NASA Formal Methods Specification and Verification Guidebook
		for Software and Computer Systems, Volume II: A Practitioner's
		Companion},
	AUTHOR = {Judith Crow and others},
	NUMBER = {NASA-GB-001-97},
	YEAR = 1997,
	ORGANIZATION = {NASA Office of Safety and Mission Assurance},
	ADDRESS = {Washington, DC},
	NOTE = {Available at \url{http://eis.jpl.nasa.gov/quality/Formal_Methods/}}
}

@inproceedings{Cyrluk&Srivas95:iccd,
	TITLE = {Theorem Proving: Not an Esoteric Diversion, but the
		Unifying Framework for Industrial Verification},
	AUTHOR = {David A. Cyrluk and Mandayam K. Srivas},
	BOOKTITLE = {International Conference on Computer Design: {VLSI}
		in Computers and Processors ({ICCD} '95)},
	PAGES = {538--544},
	MONTH = oct,
	YEAR = 1995,
	ORGANIZATION = {IEEE Computer Society},
	ADDRESS = {Austin, TX}
}

@article{Dill&Rushby96,
	TITLE = {Acceptance of Formal Methods: Lessons from Hardware
		Design},
	AUTHOR = {David L. Dill and John Rushby},
	JOURNAL = {IEEE Computer},
	PAGES = {23--24},
	VOLUME = 29,
	NUMBER = 4,
	MONTH = apr,
	YEAR = 1996,
	NOTE = {Part of~\cite{Saiedian96}}
}

@inproceedings{Rushby92:repsa,
	TITLE = {Formal Methods for Dependable Real-Time Systems},
	AUTHOR = {John Rushby},
	BOOKTITLE = {International Symposium on Real-Time Embedded Processing
		for Space Applications},
	PAGES = {355--366},
	MONTH = nov,
	YEAR = 1992,
	ORGANIZATION = {CNES, the French Space Agency},
	ADDRESS = {Les Saintes-Maries-de-la-Mer, France},
	NOTE = {Published by C\'{e}padu\`{e}s-\'{E}ditions, Toulouse,
		France}
}

@inproceedings{Rushby95:ZUM,
	TITLE = {Mechanizing Formal Methods: Opportunities and Challenges},
	AUTHOR = {John Rushby},
	BOOKTITLE = {{ZUM} '95: The {Z} Formal Specification Notation;
		9th International Conference of {Z} Users},
	EDITOR = {Jonathan P. Bowen and Michael G. Hinchey},
	PAGES = {105--113},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 967,
	MONTH = sep,
	YEAR = 1995,
	ADDRESS = {Limerick, Ireland}
}

@inproceedings{Rushby96:CAV,
	TITLE = {Automated Deduction and Formal Methods},
	AUTHOR = {John Rushby},
	BOOKTITLE = {Computer-Aided Verification, CAV '96},
	EDITOR = {Rajeev Alur and Thomas A. Henzinger},
	PAGES = {169--183},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1102,
	MONTH = {July/August},
	YEAR = 1996,
	ADDRESS = {New Brunswick, NJ}
}

@inproceedings{Rushby96:FSTTCS,
	TITLE = {Mechanized Formal Methods: Progress and Prospects},
	AUTHOR = {John Rushby},
	BOOKTITLE = {16th Conference on the Foundations of Software Technology
		and Theoretical Computer Science},
	EDITOR = {V. Chandru and V. Vinay},
	PAGES = {43--51},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1180,
	MONTH = dec,
	YEAR = 1996,
	ADDRESS = {Hyderabad, India}
}

@inproceedings{Rushby97:isre,
	TITLE = {Calculating with Requirements},
	AUTHOR = {John Rushby},
	BOOKTITLE = {3rd IEEE International Symposium on Requirements
		Engineering},
	PAGES = {144--146},
	MONTH = jan,
	YEAR = 1997,
	ORGANIZATION = {IEEE Computer Society},
	ADDRESS = {Annapolis, MD}
}

@inproceedings{Rushby:FM99,
	TITLE = {Mechanized Formal Methods: Where Next?},
	AUTHOR = {John Rushby},
	BOOKTITLE = {FM99: The World Congress in Formal Methods},
	EDITOR = {Jeannette Wing and Jim Woodcock},
	PAGES = {48--51},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = {1708 and 1709},
	MONTH = sep,
	YEAR = 1999,
	ADDRESS = {Toulouse, France},
	NOTE = {Pages 1--938 are in the first volume, 939--1872 in the
		second.}
}

@article{Shankar85,
	TITLE = {Towards Mechanical Metamathematics},
	AUTHOR = {N. Shankar},
	JOURNAL = {Journal of Automated Reasoning},
	PAGES = {407--434},
	VOLUME = 1,
	NUMBER = 4,
	YEAR = 1985
}

@article{Shankar:notes,
	TITLE = {Observations on the Use of Computers in Proof Checking},
	AUTHOR = {N. Shankar},
	JOURNAL = {Notices of the American Mathematical Society},
	PAGES = {804--805},
	VOLUME = 35,
	NUMBER = 6,
	MONTH = {July/August},
	YEAR = 1988
}

@book{Shankar:book,
	TITLE = {Metamathematics, Machines, and {G{\"o}del's} Proof},
	AUTHOR = {N. Shankar},
	PUBLISHER = {Cambridge University Press},
	SERIES = {Cambridge Tracts in Theoretical Computer Science},
	YEAR = 1994,
	ADDRESS = {Cambridge, UK}
}

@inproceedings{Shankar:FTRTFT96,
	TITLE = {Unifying Verification Paradigms},
	AUTHOR = {Natarajan Shankar},
	BOOKTITLE = {Formal Techniques in Real-Time and Fault-Tolerant
		Systems},
	EDITOR = {Bengt Jonsson and Joachim Parrow},
	PAGES = {22--39},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1135,
	MONTH = sep,
	YEAR = 1996,
	ADDRESS = {Uppsala, Sweden}
}

@techreport{Rushby:FAA-full,
	TITLE = {Formal Methods and the Certification of Critical Systems},
	AUTHOR = {John Rushby},
	NUMBER = {SRI-CSL-93-7},
	MONTH = dec,
	YEAR = 1993,
	INSTITUTION = {Computer Science Laboratory, SRI International},
	ADDRESS = {Menlo Park, CA},
	NOTE = {Also issued under the title {\em Formal Methods and Digital
		Systems Validation for Airborne Systems\/} as NASA Contractor
		Report 4551, December 1993. A book based on this material
		will be published by Cambridge University Press in 1998/9}
}

@article{Rushby94:Taxonomy,
	TITLE = {Critical System Properties: Survey and Taxonomy},
	AUTHOR = {John Rushby},
	JOURNAL = {Reliability Engineering and System Safety},
	PAGES = {189--219},
	VOLUME = 43,
	NUMBER = 2,
	YEAR = 1994
}

@techreport{Rushby:FAA-short,
	TITLE = {Formal Methods and their Role in the Certification of
		Critical Systems},
	AUTHOR = {John Rushby},
	NUMBER = {SRI-CSL-95-1},
	MONTH = mar,
	YEAR = 1995,
	INSTITUTION = {Computer Science Laboratory, SRI International},
	ADDRESS = {Menlo Park, CA},
	NOTE = {Also available as NASA Contractor Report 4673, August
		1995, and issued as part of the {\em FAA Digital Systems
		Validation Handbook} (the guide for aircraft certification).
		Reprinted in~\cite[pp.~1--42]{Encress95}}
}

@incollection{Srivas97:chapter,
	TITLE = {Hardware Verification Using {PVS}},
	AUTHOR = {Mandayam Srivas and Harald Rue{\ss} and David Cyrluk},
	BOOKTITLE = {Formal Hardware Verification: Methods and Systems
		in Comparison},
	EDITOR = {Thomas Kropf},
	PAGES = {156--205},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1287,
	YEAR = 1997
}

@inproceedings{Cyrluk96:DP,
	TITLE = {On {Shostak's} Decision Procedure for Combinations of
		Theories},
	AUTHOR = {David Cyrluk and Patrick Lincoln and N. Shankar},
	BOOKTITLE = {Automated Deduction---{CADE-13}},
	EDITOR = {M. A. McRobbie and J. K. Slaney},
	PAGES = {463--477},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Artificial Intelligence},
	VOLUME = 1104,
	MONTH = {July/August},
	YEAR = 1996,
	ADDRESS = {New Brunswick, NJ}
}

@inproceedings{Cyrluk-etal97:CAV,
	TITLE = {An Efficient Decision Procedure for the Theory of Fixed-Sized
		Bit-Vectors},
	AUTHOR = {David Cyrluk and Harald Rue{\ss} and Oliver M{\"o}ller},
	BOOKTITLE = {Computer-Aided Verification, CAV '97},
	EDITOR = {Orna Grumberg},
	PAGES = {60--71},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1254,
	MONTH = jun,
	YEAR = 1997,
	ADDRESS = {Haifa, Israel}
}

@inproceedings{Cyrluk94:gtl,
	TITLE = {Ground Temporal Logic---A Logic for Hardware Verification},
	AUTHOR = {D. Cyrluk and P. Narendran},
	BOOKTITLE = {Computer-Aided Verification, CAV '94},
	EDITOR = {David Dill},
	PAGES = {247--259},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 818,
	MONTH = jun,
	YEAR = 1994,
	ADDRESS = {Stanford, CA}
}

@inproceedings{Cyrluk94:TPCD,
	TITLE = {Effective Theorem Proving for Hardware Verification},
	AUTHOR = {D. Cyrluk and S. Rajan and N. Shankar and M. K. Srivas},
	BOOKTITLE = {Theorem Provers in Circuit Design ({TPCD} '94)},
	EDITOR = {Ramayya Kumar and Thomas Kropf},
	PAGES = {203--222},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 910,
	MONTH = sep,
	YEAR = 1994,
	ADDRESS = {Bad Herrenalb, Germany}
}

@inproceedings{Moeller98:FMCAD,
	TITLE = {Solving Bit-Vector Equations},
	AUTHOR = {Oliver M{\"o}ller and Harald Rue{\ss}},
	BOOKTITLE = {Formal Methods in Computer-Aided Design (FMCAD '98)},
	EDITOR = {Ganesh Gopalakrishnan and Phillip Windley},
	PAGES = {36--48},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1522,
	MONTH = nov,
	YEAR = 1998,
	ADDRESS = {Palo Alto, CA}
}

@inproceedings{Tiwari-etal00:CADE,
	TITLE = {Rigid E-Unification Revisited},
	AUTHOR = {Ashish Tiwari and Leo Bachmair and Harald Rue{\ss}},
	BOOKTITLE = {Automated Deduction---{CADE-17}},
	EDITOR = {David McAllester},
	PAGES = {220--234},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Artificial Intelligence},
	VOLUME = 1831,
	MONTH = jun,
	YEAR = 2000,
	ADDRESS = {Pittsburgh, PA}
}

@inproceedings{Rajan95:CAV,
	TITLE = {An Integration of Model-Checking with Automated Proof
		Checking},
	AUTHOR = {S. Rajan and N. Shankar and M.K. Srivas},
	BOOKTITLE = {Computer-Aided Verification, CAV '95},
	EDITOR = {Pierre Wolper},
	PAGES = {84--97},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 939,
	MONTH = jun,
	YEAR = 1995,
	ADDRESS = {Liege, Belgium}
}

@inproceedings{pvs-tables:tacas97,
	TITLE = {Integration in {PVS}: Tables, Types, and Model Checking},
	AUTHOR = {Sam Owre and John Rushby and N. Shankar},
	BOOKTITLE = {Tools and Algorithms for the Construction and Analysis
		of Systems {(TACAS '97)}},
	EDITOR = {Ed Brinksma},
	PAGES = {366-383},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1217,
	MONTH = apr,
	YEAR = 1997,
	ADDRESS = {Enschede, The Netherlands}
}

@inproceedings{Owre&Ruess00:CAV,
	TITLE = {Integrating {WS1S} with {PVS}},
	AUTHOR = {Sam Owre and Harald Rue{\ss}},
	BOOKTITLE = {Computer-Aided Verification, CAV '2000},
	EDITOR = {E. A. Emerson and A. P. Sistla},
	PAGES = {548--551},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1855,
	MONTH = jul,
	YEAR = 2000,
	ADDRESS = {Chicago, IL}
}

@inproceedings{Pfab98:tools,
	TITLE = {Towards Light-Weight Verification and Heavy-Weight Testing},
	AUTHOR = {Friedrich von Henke and Stephan Pfab and Harald Rue{\ss}
		and Sam Owre},
	BOOKTITLE = {Tool Support for System Specification, Development,
		and Verification},
	EDITOR = {Rudolph Berghammer and Yassine Lakhnech},
	PAGES = {189--200},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Advances in Computing Science},
	MONTH = jun,
	YEAR = 1998,
	ADDRESS = {Malente, Germany},
	NOTE = {Proceedings published in May 1999}
}

@inproceedings{vonHenke98:tphols,
	TITLE = {Case Studies in Meta-Level Theorem Proving},
	AUTHOR = {Friedrich von Henke and Stephan Pfab and Holger Pfeifer
		and Harald Rue{\ss}},
	BOOKTITLE = {Theorem Proving in Higher Order Logics: 11th International
		Conference, {TPHOLs '98}},
	EDITOR = {Jim Grundy and Malcolm Newey},
	PAGES = {461--478},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1479,
	MONTH = sep,
	YEAR = 1998,
	ADDRESS = {Canberra, Australia}
}

@techreport{shankar99:eval,
	TITLE = {Efficiently Executing {PVS}},
	AUTHOR = {N. Shankar},
	TYPE = {Project report},
	MONTH = nov,
	YEAR = 1999,
	INSTITUTION = {Computer Science Laboratory, SRI International},
	ADDRESS = {Menlo Park, CA},
	NOTE = {Available at \url{http://www.csl.sri.com/shankar/PVSeval.ps.gz}}
}

@inproceedings{Bensalem96:CAV,
	TITLE = {Powerful Techniques for the Automatic Generation of
		Invariants},
	AUTHOR = {Saddek Bensalem and Yassine Lakhnech and Hassen Sa{\"\i}di},
	BOOKTITLE = {Computer-Aided Verification, CAV '96},
	EDITOR = {Rajeev Alur and Thomas A. Henzinger},
	PAGES = {323--335},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1102,
	MONTH = {July/August},
	YEAR = 1996,
	ADDRESS = {New Brunswick, NJ}
}

@inproceedings{Bensalem98:CAV,
	TITLE = {Computing Abstractions of Infinite State Systems Compositionally
		and Automatically},
	AUTHOR = {Saddek Bensalem and Yassine Lakhnech and Sam Owre},
	BOOKTITLE = {Computer-Aided Verification, CAV '98},
	EDITOR = {Alan J. Hu and Moshe Y. Vardi},
	PAGES = {319--331},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1427,
	MONTH = jun,
	YEAR = 1998,
	ADDRESS = {Vancouver, Canada}
}

@inproceedings{Abdulla:CAV99,
	TITLE = {Verification of Infinite-State Systems by Combining
		Abstraction and Reachability Analysis},
	AUTHOR = {Parosh Aziz Abdulla and Aurore Annichini and Saddek
		Bensalem and Ahmed Bouajjani and Peter Habermehl and
		Yassine Lakhnech},
	BOOKTITLE = {Computer-Aided Verification, CAV '99},
	EDITOR = {Nicolas Halbwachs and Doron Peled},
	PAGES = {146--159},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1633,
	MONTH = jul,
	YEAR = 1999,
	ADDRESS = {Trento, Italy}
}

@inproceedings{Rusu&Singerman99,
	TITLE = {On Proving Safety Properties by Integrating Static Analysis,
		Theorem Proving and Abstraction},
	AUTHOR = {Vlad Rusu and Eli Singerman},
	BOOKTITLE = {Tools and Algorithms for the Construction and Analysis
		of Systems {(TACAS '99)}},
	EDITOR = {W. Rance Cleaveland},
	PAGES = {178--192},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1579,
	MONTH = mar,
	YEAR = 1999,
	ADDRESS = {Amsterdam, The Netherlands}
}

@inproceedings{Graf96:CAV,
	TITLE = {Verifying Invariants Using Theorem Proving},
	AUTHOR = {Susanne Graf and Hassen Sa{\"\i}di},
	BOOKTITLE = {Computer-Aided Verification, CAV '96},
	EDITOR = {Rajeev Alur and Thomas A. Henzinger},
	PAGES = {196--207},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1102,
	MONTH = {July/August},
	YEAR = 1996,
	ADDRESS = {New Brunswick, NJ}
}

@inproceedings{Saidi96,
	TITLE = {A Tool for Proving Invariance Properties of Concurrent
		Systems Automatically},
	AUTHOR = {Hassen Sa{\"\i}di},
	BOOKTITLE = {Tools and Algorithms for the Construction and Analysis
		of Systems {TACAS '96}},
	PAGES = {412--416},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1055,
	MONTH = mar,
	YEAR = 1996,
	ADDRESS = {Passau, Germany}
}

@inproceedings{Saidi97:CAV,
	TITLE = {{The Invariant Checker}: Automated Deductive Verification
		of Reactive Systems},
	AUTHOR = {Hassen Sa{\"\i}di},
	BOOKTITLE = {Computer-Aided Verification, CAV '97},
	EDITOR = {Orna Grumberg},
	PAGES = {436--439},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1254,
	MONTH = jun,
	YEAR = 1997,
	ADDRESS = {Haifa, Israel}
}

@inproceedings{Saidi&Graf97:CAV,
	TITLE = {Construction of Abstract State Graphs with {PVS}},
	AUTHOR = {Hassen Sa{\"\i}di and Susanne Graf},
	BOOKTITLE = {Computer-Aided Verification, CAV '97},
	EDITOR = {Orna Grumberg},
	PAGES = {72--83},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1254,
	MONTH = jun,
	YEAR = 1997,
	ADDRESS = {Haifa, Israel}
}

@inproceedings{Saidi97:LFM,
	TITLE = {Automated Deductive Verification of Parallel Systems},
	AUTHOR = {Hassen Sa{\"\i}di},
	BOOKTITLE = {LFM' 97: Fourth NASA Langley Formal Methods Workshop},
	EDITOR = {C. Michael Holloway and Kelly J. Hayhurst},
	PAGES = {163--176},
	SERIES = {NASA Conference Publication 3356},
	MONTH = sep,
	YEAR = 1997,
	ORGANIZATION = {NASA Langley Research Center},
	ADDRESS = {Hampton, VA},
	NOTE = {Available at \url{http://atb-www.larc.nasa.gov/Lfm97/proceedings/}}
}

@inproceedings{Saidi&Shankar:CAV99,
	TITLE = {Abstract and Model Check While You Prove},
	AUTHOR = {Hassen Sa{\"\i}di and N. Shankar},
	BOOKTITLE = {Computer-Aided Verification, CAV '99},
	EDITOR = {Nicolas Halbwachs and Doron Peled},
	PAGES = {443--454},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1633,
	MONTH = jul,
	YEAR = 1999,
	ADDRESS = {Trento, Italy}
}

@inproceedings{Saidi00:SAS,
	TITLE = {Model Checking Guided Abstraction and Analysis},
	AUTHOR = {Hassen Sa\"{\i}di},
	BOOKTITLE = {Seventh International Static Analysis Symposium
		{(SAS'00)}},
	EDITOR = {Jens Palsberg},
	PAGES = {377--396},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1824,
	MONTH = jun,
	YEAR = 2000,
	ADDRESS = {Santa Barbara CA}
}

@inproceedings{Shankar00:ASM,
	TITLE = {Symbolic Analysis of Transition Systems},
	AUTHOR = {Natarajan Shankar},
	BOOKTITLE = {Abstract State Machines: Theory and Applications
		({ASM} 2000)},
	EDITOR = {Yuri Gurevich and Phillip W. Kutter and Martin Odersky
		and Lothar Thiele},
	PAGES = {287--302},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	NUMBER = 1912,
	MONTH = mar,
	YEAR = 2000,
	ADDRESS = {Monte Verit\`{a}, Switzerland}
}

@inproceedings{Shankar00:CONCUR,
	TITLE = {Combining Theorem Proving and Model Checking through
		Symbolic Analysis},
	AUTHOR = {Natarajan Shankar},
	BOOKTITLE = {{CONCUR 2000}: Concurrency Theory},
	PAGES = {1--16},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	NUMBER = 1877,
	MONTH = aug,
	YEAR = 2000,
	ADDRESS = {State College, PA}
}

@inproceedings{Bensalem98:InVeSt,
	TITLE = {{InVeSt: A} Tool for the Verification of Invariants},
	AUTHOR = {Saddek Bensalem and Yassine Lakhnech and Sam Owre},
	BOOKTITLE = {Computer-Aided Verification, CAV '98},
	EDITOR = {Alan J. Hu and Moshe Y. Vardi},
	PAGES = {505--510},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1427,
	MONTH = jun,
	YEAR = 1998,
	ADDRESS = {Vancouver, Canada}
}

@inproceedings{SALoverview00:LFM,
	TITLE = {An Overview of {SAL}},
	AUTHOR = {Saddek Bensalem and Vijay Ganesh and Yassine Lakhnech
		and C\'{e}sar Mu{\~{n}}oz and Sam Owre and Harald Rue{\ss}
		and John Rushby and Vlad Rusu and Hassen Sa{\"\i}di and
		N. Shankar and Eli Singerman and Ashish Tiwari},
	BOOKTITLE = {LFM 2000: Fifth NASA Langley Formal Methods Workshop},
	EDITOR = {C. Michael Holloway},
	PAGES = {187--196},
	MONTH = jun,
	YEAR = 2000,
	ORGANIZATION = {NASA Langley Research Center},
	ADDRESS = {Hampton, VA},
	NOTE = {Proceedings available at \url{http://shemesh.larc.nasa.gov/fm/Lfm2000/Proc/}}
}

@inproceedings{Rushby98:ICFEM,
	TITLE = {Ubiquitous Abstraction: A New Approach for Mechanized
		Formal Verification (Extended Abstract)},
	AUTHOR = {John Rushby},
	BOOKTITLE = {Second International Conference on Formal Engineering
		Methods (ICFEM '98)},
	EDITOR = {John Staples and Michael G. Hinchey and Shaoying Liu},
	PAGES = {176--178},
	MONTH = dec,
	YEAR = 1998,
	ORGANIZATION = {IEEE Computer Society},
	ADDRESS = {Brisbane, Australia}
}

@inproceedings{Rushby:SPIN99,
	TITLE = {Integrated Formal Verification: Using Model Checking
		With Automated Abstraction, Invariant Generation, and
		Theorem Proving},
	AUTHOR = {John Rushby},
	BOOKTITLE = {Theoretical and Practical Aspects of SPIN Model
		Checking: 5th and 6th International SPIN Workshops},
	EDITOR = {D. Dams and R. Gerth and S. Leue and M. Massink},
	PAGES = {1--11},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1680,
	MONTH = {July and September},
	YEAR = 1999,
	ADDRESS = {Trento, Italy, and Toulouse, France}
}

@inproceedings{Rushby00:Forte,
	TITLE = {From Refutation to Verification},
	AUTHOR = {John Rushby},
	BOOKTITLE = {Formal Description Techniques and Protocol Specification,
		Testing and Verification {FORTE XIII/PSTV XX 2000}},
	EDITOR = {Tommaso Bolognesi and Diego Latella},
	PAGES = {369--374},
	PUBLISHER = {Kluwer Academic Publishers},
	MONTH = oct,
	YEAR = 2000,
	ADDRESS = {Pisa, Italy}
}

@inproceedings{Rushby00:HASE,
	TITLE = {Disappearing Formal Methods},
	AUTHOR = {John Rushby},
	BOOKTITLE = {High-Assurance Systems Engineering Symposium},
	PAGES = {95--96},
	MONTH = nov,
	YEAR = 2000,
	ORGANIZATION = {Association for Computing Machinery},
	ADDRESS = {Albuquerque, NM}
}

@article{Young97:IC,
	TITLE = {Comparing Verification Systems: {Interactive Consistency}
		in {ACL2}},
	AUTHOR = {William D. Young},
	JOURNAL = {IEEE Transactions on Software Engineering},
	PAGES = {214--223},
	VOLUME = 23,
	NUMBER = 4,
	MONTH = apr,
	YEAR = 1997
}

@inproceedings{Miner95:HOL,
	TITLE = {Specification of the {IEEE-854} Floating-Point Standard
		in {HOL} and {PVS}},
	AUTHOR = {Victor A. {Carre{\~{n}}o} and Paul S. Miner},
	BOOKTITLE = {{HOL95}: Eighth International Workshop on Higher-Order
		Logic Theorem Proving and Its Applications},
	MONTH = sep,
	YEAR = 1995,
	ADDRESS = {Aspen Grove, UT},
	NOTE = {Category B proceedings, available at \url{http://lal.cs.byu.edu/lal/hol95/Bprocs/indexB.html}}
}

@misc{Gordon95:PVS,
	TITLE = {Notes on {PVS} from a {HOL} Perspective},
	AUTHOR = {Mike Gordon},
	HOWPUBLISHED = {Available at \url{http://www.cl.cam.ac.uk/users/mjcg/PVS.html}},
	MONTH = aug,
	YEAR = 1995,
	INSTITUTION = {Cambridge University}
}

@inproceedings{Griffioen98:tphols,
	TITLE = {A Comparison of {PVS} and {Isabelle/HOL}},
	AUTHOR = {David Griffioen and Marieke Huisman},
	BOOKTITLE = {Theorem Proving in Higher Order Logics: 11th International
		Conference, {TPHOLs '98}},
	EDITOR = {Jim Grundy and Malcolm Newey},
	PAGES = {123--142},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1479,
	MONTH = sep,
	YEAR = 1998,
	ADDRESS = {Canberra, Australia}
}

@inproceedings{Groote-etal98:CONCUR,
	TITLE = {Checking Verifications of Protocols and Distributed
		Systems by Computer},
	AUTHOR = {Jan Friso Groote and Fran\,{c}ois Monin and Jaco van
		de Pol},
	BOOKTITLE = {{CONCUR'98}: Concurrency Theory},
	EDITOR = {Davide Sangiorgi and Robert de Simone},
	PAGES = {629--655},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1466,
	MONTH = sep,
	YEAR = 1998,
	ADDRESS = {Nice, France}
}

@article{Kern99:todaes,
	TITLE = {Formal Verification in Hardware Design: A Survey},
	AUTHOR = {Christoph Kern and Mark R. Greenstreet},
	JOURNAL = {ACM Transactions on Design Automation of Electronic
		Systems (TODAES)},
	PAGES = {123--193},
	VOLUME = 4,
	NUMBER = 2,
	MONTH = apr,
	YEAR = 1999
}

@inproceedings{Rust98,
	TITLE = {A {PVS} Specification of an Invoicing System},
	AUTHOR = {Heinrich Rust},
	BOOKTITLE = {Proceedings of an International Workshop on Specification
		Techniques and Formal Methods},
	EDITOR = {M. Allemand and C. Attiogb\'{e} and H. Habrias},
	PAGES = {51--65},
	MONTH = mar,
	YEAR = 1998,
	ORGANIZATION = {University of Nantes, France},
	NOTE = {Available at \url{http://www.informatik.tu-cottbus.de/~rust/publications/a_pvs_specificat%
		ion_of_an_invoicing_system.ps.gz}}
}

@inproceedings{Wilding97:LFM,
	TITLE = {Robust Computer System Proofs in {PVS}},
	AUTHOR = {Matthew Wilding},
	BOOKTITLE = {LFM' 97: Fourth NASA Langley Formal Methods Workshop},
	EDITOR = {C. Michael Holloway and Kelly J. Hayhurst},
	PAGES = {177--184},
	SERIES = {NASA Conference Publication 3356},
	MONTH = sep,
	YEAR = 1997,
	ORGANIZATION = {NASA Langley Research Center},
	ADDRESS = {Hampton, VA},
	NOTE = {Available at \url{http://atb-www.larc.nasa.gov/Lfm97/proceedings/}}
}

@inproceedings{Droschl:IFMW99,
	TITLE = {On the Integration of Formal Methods: Events and Scenarios
		in {PVS} and {VDM}},
	AUTHOR = {Georg Droschl},
	BOOKTITLE = {Proceedings, 3rd. Irish Workshop in Formal Methods},
	PUBLISHER = {Electronic Workshops in Computing (\url{http://ewic.org.uk/ewic/})},
	MONTH = jul,
	YEAR = 1999,
	ADDRESS = {Galway, Ireland}
}

@inproceedings{Droschl:FM99,
	TITLE = {Analyzing the Requirements of an Access Control Using
		{VDMTools} and {PVS}},
	AUTHOR = {Georg Droschl},
	BOOKTITLE = {FM99: The World Congress in Formal Methods},
	EDITOR = {Jeannette Wing and Jim Woodcock},
	PAGES = 1807,
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = {1708 and 1709},
	MONTH = sep,
	YEAR = 1999,
	ADDRESS = {Toulouse, France},
	NOTE = {Pages 1--938 are in the first volume, 939--1872 in the
		second.}
}

@inproceedings{Merriam96,
	TITLE = {Evaluating the Interfaces of Three Theorem Proving Assistants},
	AUTHOR = {Nicholas A. Merriam and Michael D. Harrison},
	BOOKTITLE = {Proceedings of the 3rd International {Eurographics}
		Workshop on Design, Specification, and Verification of
		Interactive Systems},
	EDITOR = {F. Bodart and J. Vanderdonckt},
	YEAR = 1996
}

@inproceedings{Archer&Heitmeyer97:TPHOLS,
	TITLE = {Human-Style Theorem Proving Using {PVS}},
	AUTHOR = {Myla Archer and Constance Heitmeyer},
	BOOKTITLE = {Theorem Proving in Higher Order Logics: 10th International
		Conference, {TPHOLs '97}},
	EDITOR = {Elsa Gunter and Amy Felty},
	PAGES = {33--48},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1275,
	MONTH = aug,
	YEAR = 1997,
	ADDRESS = {Murray Hill, NJ}
}

@inproceedings{Archer98:UITP,
	TITLE = {{TAME: A PVS} Interface to Simplify Proofs for Automata
		Models},
	AUTHOR = {Myla Archer and Constance Heitmeyer and Steve Sims},
	BOOKTITLE = {User Interfaces for Theorem Provers},
	MONTH = jul,
	YEAR = 1998,
	ADDRESS = {Eindhoven, The Netherlands},
	NOTE = {Informal proceedings available at \url{http://www.win.tue.nl/cs/ipa/uitp/proceedings.html}}
}

@inproceedings{Knight97:LFM,
	TITLE = {Why Are Formal Methods Not Used More Widely?},
	AUTHOR = {John Knight and Colleen DeJong and Matthew Gibble and
		Lu{\'\i}s Nakano},
	BOOKTITLE = {LFM' 97: Fourth NASA Langley Formal Methods Workshop},
	EDITOR = {C. Michael Holloway and Kelly J. Hayhurst},
	PAGES = {1--12},
	SERIES = {NASA Conference Publication 3356},
	MONTH = sep,
	YEAR = 1997,
	ORGANIZATION = {NASA Langley Research Center},
	ADDRESS = {Hampton, VA},
	NOTE = {Available at \url{http://atb-www.larc.nasa.gov/Lfm97/proceedings/}}
}

@inproceedings{Dutertre96,
	TITLE = {Elements of Mathematical Analysis in {PVS}},
	AUTHOR = {Bruno Dutertre},
	BOOKTITLE = {Theorem Proving in Higher Order Logics: 9th International
		Conference, {TPHOLs '96}},
	EDITOR = {Joakim von Wright and Jim Grundy and John Harrison},
	PAGES = {141--156},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1125,
	MONTH = aug,
	YEAR = 1996,
	ADDRESS = {Turku, Finland}
}

@inproceedings{Gottliebsen00:TPHOLS,
	TITLE = {Transcendental Functions and Continuity Checking in
		{PVS}},
	AUTHOR = {Hanne Gottliebsen},
	BOOKTITLE = {Theorem Proving in Higher Order Logics: 13th International
		Conference, {TPHOLs 2000}},
	EDITOR = {Mark Aargaard and John Harrison},
	PAGES = {197--214},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1869,
	MONTH = aug,
	YEAR = 2000,
	ADDRESS = {Portland, OR}
}

@inproceedings{Basten&Hooman99,
	TITLE = {Process Algebra in {PVS}},
	AUTHOR = {Twan Basten and Jozef Hooman},
	BOOKTITLE = {Tools and Algorithms for the Construction and Analysis
		of Systems {(TACAS '99)}},
	EDITOR = {W. Rance Cleaveland},
	PAGES = {270--284},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1579,
	MONTH = mar,
	YEAR = 1999,
	ADDRESS = {Amsterdam, The Netherlands}
}

@inproceedings{Schamschurko98,
	TITLE = {Modeling Process Calculi With {PVS}},
	AUTHOR = {Dmitri Schamschurko},
	BOOKTITLE = {First Workshop on Coalgebraic Methods in Computer
		Science {(CMCS'98)}},
	EDITOR = {B. Jacobs and L. Moss and H. Reichel and J. Rutten},
	PAGES = {197--214},
	PUBLISHER = {Elsevier},
	SERIES = {Electronic Notes in Theoretical Computer Science},
	VOLUME = 11,
	MONTH = mar,
	YEAR = 1998,
	ADDRESS = {Lisbon, Portugal},
	NOTE = {Available at \url{http://www.elsevier.nl/cas/tree/store/tcs/free/entcs/store/tcs11/tcs110%
		11.ps}}
}

@inproceedings{Griffioen98:CAV,
	TITLE = {Normed Simulations},
	AUTHOR = {David Griffioen and Frits Vaandrager},
	BOOKTITLE = {Computer-Aided Verification, CAV '98},
	EDITOR = {Alan J. Hu and Moshe Y. Vardi},
	PAGES = {332--344},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1427,
	MONTH = jun,
	YEAR = 1998,
	ADDRESS = {Vancouver, Canada}
}

@inproceedings{Pnueli98:FTRTFT,
	TITLE = {Fair Synchronous Transition Systems and their Liveness
		Proofs},
	AUTHOR = {Amir Pnueli and N. Shankar and Eli Singerman},
	BOOKTITLE = {Formal Techniques in Real-Time and Fault-Tolerant
		Systems},
	PAGES = {198--209},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1486,
	MONTH = sep,
	YEAR = 1998,
	ADDRESS = {Lyngby, Denmark}
}

@inproceedings{Devillers-etal97,
	TITLE = {Possibly Infinite Sequences in Theorem Provers: A Comparative
		Study},
	AUTHOR = {M. Devillers and D. Griffioen and O. Mueller},
	BOOKTITLE = {Theorem Proving in Higher Order Logics: 10th International
		Conference, {TPHOLs '97}},
	EDITOR = {Elsa Gunter and Amy Felty},
	PAGES = {89--104},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1275,
	MONTH = aug,
	YEAR = 1997,
	ADDRESS = {Murray Hill, NJ}
}

@inproceedings{Hensel&Jacobs97,
	TITLE = {Proof Principles for Datatypes with Iterated Recursion},
	AUTHOR = {Ulrich Hensel and Bart Jacobs},
	BOOKTITLE = {Category Theory and Computer Science},
	EDITOR = {Eugenio Moggi and Giuseppe Rosolini},
	PAGES = {220--241},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1290,
	MONTH = sep,
	YEAR = 1997,
	ADDRESS = {Santa Margherita Ligure, Italy}
}

@article{Hensel98:JLC,
	TITLE = {Coalgebraic Theories of Sequences in {PVS}},
	AUTHOR = {Ulrich Hensel and Bart Jacobs},
	JOURNAL = {Journal of Logic and Computation},
	PAGES = {463--500},
	VOLUME = 9,
	NUMBER = 4,
	YEAR = 1999
}

@inproceedings{Hensel-etal98,
	TITLE = {Reasoning About Classes in Object-Oriented Languages:
		Logical Models and Tools},
	AUTHOR = {Ulrich Hensel and Marieke Huisman and Bart Jacobs and
		Hendrik Tews},
	BOOKTITLE = {Programming Languages and Systems: 7th European
		Symposium On Programming {(ESOP)}},
	EDITOR = {Chris Hankin},
	PAGES = {105--121},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1381,
	MONTH = mar,
	YEAR = 1998,
	ADDRESS = {Lisbon, Portugal}
}

@inproceedings{Huisman-etal99:ECOOP,
	TITLE = {A Case Study in Class Library Verification: {Java's}
		Vector Class},
	AUTHOR = {Marieke Huisman and Bart Jacobs and Joachim van den
		Berg},
	BOOKTITLE = {Object-Oriented Technology: ECOOP'99 Workshop Reader},
	EDITOR = {A. Moreira and D. Demeyer},
	PAGES = {109---110},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1743,
	MONTH = jun,
	YEAR = 1999,
	ADDRESS = {Lisbon, Portugal}
}

@inproceedings{Jacobs98:OOPSLA,
	TITLE = {Reasoning about {Java} Classes},
	AUTHOR = {Bart Jacobs and Joachim van den Berg and Marieke Huisman
		and Martijn van Berkum and Ulrich Hensel and Hendrick
		Tews},
	BOOKTITLE = {Proceedings, Object-Oriented Programming Systems,
		Languages and Applications (OOPSLA'98)},
	PAGES = {329--340},
	MONTH = oct,
	YEAR = 1998,
	ORGANIZATION = {Association for Computing Machinery},
	ADDRESS = {Vancouver, Canada},
	NOTE = {Proceedings issued as ACM SIGPLAN Notices Vol.~33, No.~10,
		October 1998.}
}

@inproceedings{Huisman&Jacobs00:TPHOLS,
	TITLE = {Inheritance in Higher Order Logic: Modeling and Reasoning},
	AUTHOR = {Marieke Huisman and Bart Jacobs},
	BOOKTITLE = {Theorem Proving in Higher Order Logics: 13th International
		Conference, {TPHOLs 2000}},
	EDITOR = {Mark Aargaard and John Harrison},
	PAGES = {301--319},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1869,
	MONTH = aug,
	YEAR = 2000,
	ADDRESS = {Portland, OR}
}

@phdthesis{Huisman:PhD,
	TITLE = {Java Program Verification in {Higher}-Order Logic with
		{PVS} and {Isabelle}},
	AUTHOR = {Marieke Huisman},
	YEAR = 2001,
	SCHOOL = {University of Nijmegen, The Netherlands}
}

@inproceedings{Huisman&Jacobs00:FASE,
	TITLE = {Java Program Verfication via a Hoare Logic with Abrupt
		Termination},
	AUTHOR = {Marieke Huisman and Bart Jacobs},
	BOOKTITLE = {Fundamental Approaches to Software Engineering,
		{FASE} 2000},
	EDITOR = {Tom Maibaum},
	PAGES = {284--303},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	NUMBER = 1783,
	MONTH = {March/April},
	YEAR = 2000,
	ADDRESS = {Berlin, Germany}
}

@inproceedings{vandenBerg-etal00:WADT,
	TITLE = {A Type-Theoretic Memory Model for Verification of Sequential
		{Java} Programs},
	AUTHOR = {Joachim van den Berg and Marieke Huisman and Bart Jacobs
		and Erik Poll},
	BOOKTITLE = {Recent Trends in Algebraic Development Techniques,
		{WADT '99}},
	EDITOR = {Didier Bert and Christine Choppy and Peter Mosses},
	PAGES = {1--21},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	NUMBER = 1827,
	MONTH = sep,
	YEAR = 1999,
	ADDRESS = {Toulouse, France}
}

@inproceedings{Lincoln&Rushby93:CAV,
	TITLE = {Formal Verification of an Algorithm for Interactive
		Consistency under a Hybrid Fault Model},
	AUTHOR = {Patrick Lincoln and John Rushby},
	BOOKTITLE = {Computer-Aided Verification, CAV '93},
	EDITOR = {Costas Courcoubetis},
	PAGES = {292--304},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 697,
	MONTH = {June/July},
	YEAR = 1993,
	ADDRESS = {Elounda, Greece}
}

@inproceedings{Lincoln&Rushby93:FTCS,
	TITLE = {A Formally Verified Algorithm for Interactive Consistency
		under a Hybrid Fault Model},
	AUTHOR = {Patrick Lincoln and John Rushby},
	BOOKTITLE = {Fault Tolerant Computing Symposium 23},
	PAGES = {402--411},
	MONTH = jun,
	YEAR = 1993,
	ORGANIZATION = {IEEE Computer Society},
	ADDRESS = {Toulouse, France},
	NOTE = {Reprinted in~\cite[pp.\ 438--447]{FTCS-highlights}}
}

@inproceedings{Lincoln&Rushby94:FTP,
	TITLE = {Formal Verification of an Interactive Consistency Algorithm
		for the {Draper FTP} Architecture Under a Hybrid Fault
		Model},
	AUTHOR = {Patrick Lincoln and John Rushby},
	BOOKTITLE = {COMPASS '94 (Proceedings of the Ninth Annual Conference
		on Computer Assurance)},
	PAGES = {107--120},
	MONTH = jun,
	YEAR = 1994,
	ORGANIZATION = {IEEE Washington Section},
	ADDRESS = {Gaithersburg, MD}
}

@inproceedings{Pfeifer99:DCCA,
	TITLE = {Formal Verification for Time-Triggered Clock Synchronization},
	AUTHOR = {Holger Pfeifer and Detlef Schwier and Friedrich W.
		von Henke},
	BOOKTITLE = {Dependable Computing for Critical Applications---7},
	EDITOR = {Charles B. Weinstock and John Rushby},
	PAGES = {207--226},
	PUBLISHER = {IEEE Computer Society},
	SERIES = {Dependable Computing and Fault Tolerant Systems},
	VOLUME = 12,
	MONTH = jan,
	YEAR = 1999,
	ADDRESS = {San Jose, CA}
}

@inproceedings{Pfeifer00:FORTE,
	TITLE = {Formal Verification of the {TTA} Group Membership Algorithm},
	AUTHOR = {Holger Pfeifer},
	BOOKTITLE = {Formal Description Techniques and Protocol Specification,
		Testing and Verification {FORTE XIII/PSTV XX 2000}},
	EDITOR = {Tommaso Bolognesi and Diego Latella},
	PAGES = {3--18},
	PUBLISHER = {Kluwer Academic Publishers},
	MONTH = oct,
	YEAR = 2000,
	ADDRESS = {Pisa, Italy}
}

@article{Rushby99:TSE,
	TITLE = {Systematic Formal Verification for Fault-Tolerant Time-Triggered
		Algorithms},
	AUTHOR = {John Rushby},
	JOURNAL = {IEEE Transactions on Software Engineering},
	PAGES = {651--660},
	VOLUME = 25,
	NUMBER = 5,
	MONTH = {September/October},
	YEAR = 1999
}

@inproceedings{Rushby00:CAV,
	TITLE = {Verification Diagrams Revisited: Disjunctive Invariants
		for Easy Verification},
	AUTHOR = {John Rushby},
	BOOKTITLE = {Computer-Aided Verification, CAV '2000},
	EDITOR = {E. A. Emerson and A. P. Sistla},
	PAGES = {508--520},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1855,
	MONTH = jul,
	YEAR = 2000,
	ADDRESS = {Chicago, IL}
}

@inproceedings{Schwier98:FTRTFT,
	TITLE = {Mechanical Verification of Clock Synchronization Algorithms},
	AUTHOR = {D. Schwier and F. von Henke},
	BOOKTITLE = {Formal Techniques in Real-Time and Fault-Tolerant
		Systems},
	PAGES = {262--271},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1486,
	MONTH = sep,
	YEAR = 1998,
	ADDRESS = {Lyngby, Denmark}
}

@article{WalterLincolnSuri97,
	TITLE = {Formally Verified On-Line Diagnosis},
	AUTHOR = {Chris J. Walter and Patrick Lincoln and Neeraj Suri},
	JOURNAL = {IEEE Transactions on Software Engineering},
	PAGES = {684--721},
	VOLUME = 23,
	NUMBER = 11,
	MONTH = nov,
	YEAR = 1997
}

@techreport{DiVito:partitioningCR,
	TITLE = {A Formal Model of Partitioning for Integrated Modular
		Avionics},
	AUTHOR = {Ben L. {Di Vito}},
	TYPE = {NASA Contractor Report},
	NUMBER = {CR-1998-208703},
	MONTH = aug,
	YEAR = 1998,
	INSTITUTION = {NASA Langley Research Center}
}

@inproceedings{diVito99:DCCA,
	TITLE = {A Model of Cooperative Noninterference for Integrated
		Modular Avionics},
	AUTHOR = {Ben L. {Di Vito}},
	BOOKTITLE = {Dependable Computing for Critical Applications---7},
	EDITOR = {Charles B. Weinstock and John Rushby},
	PAGES = {269--286},
	PUBLISHER = {IEEE Computer Society},
	SERIES = {Dependable Computing and Fault Tolerant Systems},
	VOLUME = 12,
	MONTH = jan,
	YEAR = 1999,
	ADDRESS = {San Jose, CA}
}

@inproceedings{Wilding99:DCCA,
	TITLE = {Invariant Performance: A Statement of Task Isolation
		Useful for Embedded Application Integration},
	AUTHOR = {Matthew M. Wilding and David S. Hardin and David A.
		Greve},
	BOOKTITLE = {Dependable Computing for Critical Applications---7},
	EDITOR = {Charles B. Weinstock and John Rushby},
	PAGES = {287--300},
	PUBLISHER = {IEEE Computer Society},
	SERIES = {Dependable Computing and Fault Tolerant Systems},
	VOLUME = 12,
	MONTH = jan,
	YEAR = 1999,
	ADDRESS = {San Jose, CA}
}

@techreport{Butler96:rqts,
	TITLE = {An Introduction to Requirements Capture Using {PVS}:
		Specification of a Simple Autopilot},
	AUTHOR = {Ricky W. Butler},
	TYPE = {NASA Technical Memorandum},
	NUMBER = 110255,
	MONTH = may,
	YEAR = 1996,
	INSTITUTION = {NASA Langley Research Center},
	ADDRESS = {Hampton, VA}
}

@article{Dutertre&Stavridou97,
	TITLE = {Formal Requirements Analysis of an Avionics Control
		System},
	AUTHOR = {Bruno Dutertre and Victoria Stavridou},
	JOURNAL = {IEEE Transactions on Software Engineering},
	PAGES = {267--278},
	VOLUME = 23,
	NUMBER = 5,
	MONTH = may,
	YEAR = 1997
}

@inproceedings{Dutertre97:LFM,
	TITLE = {Requirements Analysis of Real-Time Control Systems Using
		{PVS}},
	AUTHOR = {Bruno Dutertre and Victoria Stavridou},
	BOOKTITLE = {LFM' 97: Fourth NASA Langley Formal Methods Workshop},
	EDITOR = {C. Michael Holloway and Kelly J. Hayhurst},
	PAGES = {65--74},
	SERIES = {NASA Conference Publication 3356},
	MONTH = sep,
	YEAR = 1997,
	ORGANIZATION = {NASA Langley Research Center},
	ADDRESS = {Hampton, VA},
	NOTE = {Available at \url{http://atb-www.larc.nasa.gov/Lfm97/proceedings/}}
}

@article{Crow&DiVito98:tosem,
	TITLE = {Formalizing {Space Shuttle} Software Requirements: Four
		Case Studies},
	AUTHOR = {Judith Crow and Ben L. {Di Vito}},
	JOURNAL = {ACM Transactions on Software Engineering and Methodology},
	PAGES = {296--332},
	VOLUME = 7,
	NUMBER = 3,
	MONTH = jul,
	YEAR = 1998
}

@article{Easterbrook-etal98,
	TITLE = {Experiences Using Lightweight Formal Methods for Requirements
		Modeling},
	AUTHOR = {Steve Easterbrook and Robyn Lutz and Richard Covington
		and John Kelly and Yoko Ampo and David Hamilton},
	JOURNAL = {IEEE Transactions on Software Engineering},
	PAGES = {4--14},
	VOLUME = 24,
	NUMBER = 1,
	MONTH = jan,
	YEAR = 1998
}

@techreport{HAC-study,
	TITLE = {Using Formal Methods to Assist in the Requirements Analysis
		of the {Space Shuttle HAC Change Request (CR 90960E)}},
	AUTHOR = {Larry W. Roberts and Mike Beims},
	NUMBER = {JSC-27599},
	MONTH = sep,
	YEAR = 1996,
	INSTITUTION = {NASA Johnson Space Center},
	ADDRESS = {Houston, TX}
}

@inproceedings{DiVito96,
	TITLE = {Formalizing New Navigation Requirements for {NASA's
		Space Shuttle}},
	AUTHOR = {Ben L. {Di Vito}},
	BOOKTITLE = {Formal Methods Europe {FME '96}},
	PAGES = {160--178},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1051,
	MONTH = mar,
	YEAR = 1996,
	ADDRESS = {Oxford, UK}
}

@article{DiVito00:STTT,
	TITLE = {High-Automation Proofs for Properties of Requirements
		Models},
	AUTHOR = {Ben L. {Di Vito}},
	JOURNAL = {Software Tools for Technology Transfer},
	VOLUME = 3,
	NUMBER = 1,
	YEAR = 2000,
	NOTE = {To appear; available at \url{http://shemesh.larc.nasa.gov/people/bld/ftp/sttt-bld.ps}}
}

@techreport{GPS-study,
	TITLE = {Using Formal Methods to Assist in the Requirements Analysis
		of the {Space Shuttle GPS Change Request}},
	AUTHOR = {Ben L. {Di Vito} and Larry W. Roberts},
	TYPE = {NASA Contractor Report},
	NUMBER = 4752,
	MONTH = aug,
	YEAR = 1996,
	INSTITUTION = {NASA Langley Research Center}
}

@inproceedings{Hamilton-etal95,
	TITLE = {Experiences in Applying Formal Methods to the Analysis
		of Software and System Requirements},
	AUTHOR = {David Hamilton and Rick Covington and John Kelly},
	BOOKTITLE = {WIFT '95: Workshop on Industrial-Strength Formal
		Specification Techniques},
	PAGES = {30--43},
	YEAR = 1995,
	ORGANIZATION = {IEEE Computer Society},
	ADDRESS = {Boca Raton, FL}
}

@inproceedings{Hamilton-etal95-2,
	TITLE = {An Experience Report on Requirements Reliability Engineering
		Using Formal Methods},
	AUTHOR = {David Hamilton and Rick Covington and Alice Lee},
	BOOKTITLE = {Sixth International Conference on Software Reliability
		Engineering, {ISSRE '95}},
	PAGES = {52--57},
	YEAR = 1995,
	ORGANIZATION = {IEEE Computer Society},
	ADDRESS = {Toulouse, France}
}

@inproceedings{Ampo&Lutz95,
	TITLE = {Evaluation of Software Safety Analysis Using Formal
		Methods},
	AUTHOR = {Yoko Ampo and Robyn Lutz},
	BOOKTITLE = {Workshop for Foundation of Software Engineering
		{(FOSE)}},
	MONTH = dec,
	YEAR = 1995,
	ADDRESS = {Hamana-Ko, Japan},
	NOTE = {In Japanese}
}

@inproceedings{Lutz&Ampo94,
	TITLE = {Experience Report: Using Formal Methods for Requirements
		Analysis of Critical Spacecraft Software},
	AUTHOR = {Robyn Lutz and Yoko Ampo},
	BOOKTITLE = {Proceedings of the 19th Annual Software Engineering
		Workshop},
	PAGES = {231--248},
	MONTH = dec,
	YEAR = 1994,
	ORGANIZATION = {NASA Goddard Space Flight Center},
	ADDRESS = {Greenbelt, MD}
}

@inproceedings{Lutz97:LFM,
	TITLE = {Reuse of a Formal Model for Requirements Validation},
	AUTHOR = {Robyn Lutz},
	BOOKTITLE = {LFM' 97: Fourth NASA Langley Formal Methods Workshop},
	EDITOR = {C. Michael Holloway and Kelly J. Hayhurst},
	PAGES = {75--86},
	SERIES = {NASA Conference Publication 3356},
	MONTH = sep,
	YEAR = 1997,
	ORGANIZATION = {NASA Langley Research Center},
	ADDRESS = {Hampton, VA},
	NOTE = {Available at \url{http://atb-www.larc.nasa.gov/Lfm97/proceedings/}}
}

@inproceedings{Carreno&Munoz00:TPHOLS,
	TITLE = {Aircraft Trajectory Modeling and Alerting Algorithm
		Verification},
	AUTHOR = {Victor Carre{\~{n}}o and C\'{e}sar Mu{\~{n}}oz},
	BOOKTITLE = {Theorem Proving in Higher Order Logics: 13th International
		Conference, {TPHOLs 2000}},
	EDITOR = {Mark Aargaard and John Harrison},
	PAGES = {90--105},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1869,
	MONTH = aug,
	YEAR = 2000,
	ADDRESS = {Portland, OR}
}

@inproceedings{Carreno&Munoz00:DASC,
	TITLE = {Formal Analysis of Parallel Landing Scenarios},
	AUTHOR = {Victor Carre{\~{n}}o and C\'{e}sar Mu{\~{n}}oz},
	BOOKTITLE = {19th AIAA/IEEE Digital Avionics Systems Conference},
	MONTH = oct,
	YEAR = 2000,
	ADDRESS = {Philadelphia, PA}
}

@inproceedings{Lawford-etal00:AMAST,
	TITLE = {Practical Application of Functional and Relational Methods
		for the Specification and Verification of Safety Critical
		Software},
	AUTHOR = {Mark Lawford and Jeff McDougall and Peter Froebel and
		Greg Moum},
	BOOKTITLE = {Algebraic Methodology and Software Technology, {AMAST}
		2000},
	EDITOR = {Teodor Rus},
	PAGES = {73--88},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1816,
	MONTH = may,
	YEAR = 2000,
	ADDRESS = {Iowa City, IA}
}

@article{Koo-etal99,
	TITLE = {Mathematical Verification of a Nuclear Power Plant Protection
		System Function With Combined {CPN} and {PVS}},
	AUTHOR = {S. Koo and H. Son and P. Seong},
	JOURNAL = {Journal of the Korean Nuclear Society},
	PAGES = {157--171},
	VOLUME = 31,
	MONTH = apr,
	YEAR = 1999
}

@inproceedings{vandePol98,
	TITLE = {Formal Requirements Specification for Command and Control
		Systems},
	AUTHOR = {Jaco van de Pol and Jozef Hooman and Edwin de Jong},
	BOOKTITLE = {Engineering of Computer Based Systems {(ECBS)}},
	PAGES = {37--44},
	MONTH = {March--April},
	YEAR = 1998,
	ORGANIZATION = {IEEE Computer Society},
	ADDRESS = {Jerusalem, Israel},
	NOTE = {Available at \url{http://www.win.tue.nl/cs/tt/hooman/ECBS98.html}}
}

@inproceedings{Dean97,
	TITLE = {Static Typing with Dynamic Linking},
	AUTHOR = {Drew Dean},
	BOOKTITLE = {Fourth ACM Conference on Computer and Communications
		Security},
	PAGES = {18--27},
	MONTH = apr,
	YEAR = 1997,
	ORGANIZATION = {Association for Computing Machinery},
	ADDRESS = {Zurich, Switzerland}
}

@inproceedings{Hoffman98:CAV,
	TITLE = {A Formal Experience at {Secure Computing Corporation}},
	AUTHOR = {John Hoffman and Charlie Payne},
	BOOKTITLE = {Computer-Aided Verification, CAV '98},
	EDITOR = {Alan J. Hu and Moshe Y. Vardi},
	PAGES = {49--56},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1427,
	MONTH = jun,
	YEAR = 1998,
	ADDRESS = {Vancouver, Canada}
}

@inproceedings{Peri96,
	TITLE = {A Logic of Composition for Information Flow Predicates},
	AUTHOR = {Ramesh V. Peri and William A. Wulf and Darrell M. Kienzle},
	BOOKTITLE = {9th Computer Security Foundations Workshop},
	PAGES = {82--94},
	MONTH = jun,
	YEAR = 1996,
	ORGANIZATION = {IEEE Computer Society},
	ADDRESS = {Kenmare, Ireland}
}

@inproceedings{Dieckman98,
	TITLE = {{ActiveSPEC}: A Framework for the Specification and
		Verification of Active Network Services and Security
		Policies},
	AUTHOR = {Darryl Dieckman and Perry Alexander and Philip A. Wilsey},
	BOOKTITLE = {Workshop on Formal Methods and Security Protocols},
	EDITOR = {Nevin Heintze and Jeannette Wing},
	MONTH = jun,
	YEAR = 1998,
	ADDRESS = {Indianapolis, IN},
	NOTE = {Informal proceedings available at \url{http://www.cs.bell-labs.com/who/nch/fmsp/program.html}}
}

@inproceedings{Dutertre&Schneider97,
	TITLE = {Embedding {CSP} in {PVS}. An Application to Authentication
		Protocols},
	AUTHOR = {Bruno Dutertre and Steve Schneider},
	BOOKTITLE = {Theorem Proving in Higher Order Logics: 10th International
		Conference, {TPHOLs '97}},
	EDITOR = {Elsa Gunter and Amy Felty},
	PAGES = {121--136},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1275,
	MONTH = aug,
	YEAR = 1997,
	ADDRESS = {Murray Hill, NJ}
}

@inproceedings{Millen:FMSP99,
	TITLE = {A Necessarily Parallel Attack},
	AUTHOR = {Jonathan K. Millen},
	BOOKTITLE = {Workshop on Formal Methods and Security Protocols,
		Part of the Federated Logic Conference},
	EDITOR = {Nevin Heintze and Edmund Clarke},
	MONTH = jul,
	YEAR = 1999,
	ADDRESS = {Trento, Italy}
}

@inproceedings{Monniaux99:CSFW,
	TITLE = {Decision Procedures for the Analysis of Cryptographic
		Protocols by Logics of Belief},
	AUTHOR = {David Monniaux},
	BOOKTITLE = {12th Computer Security Foundations Workshop},
	PAGES = {44--54},
	MONTH = jun,
	YEAR = 1999,
	ORGANIZATION = {IEEE Computer Society},
	ADDRESS = {Mordano, Italy}
}

@inproceedings{Ruess&Millen00:FMCS,
	TITLE = {Local Secrecy for State-Based Models},
	AUTHOR = {Harald Rue{\ss} and Jonathan Millen},
	BOOKTITLE = {Formal Methods and Computer Security (FMCS)},
	MONTH = jul,
	YEAR = 2000,
	ADDRESS = {Chicago, IL}
}

@inproceedings{Gopi98:FSTTCS,
	TITLE = {Formal Verification of an {O.S.} Submodule},
	AUTHOR = {N.S. Pendharkar and K. Gopinath},
	BOOKTITLE = {18th Conference on the Foundations of Software Technology
		and Theoretical Computer Science},
	EDITOR = {V. Arvind and R. Ramanujin},
	PAGES = {197--208},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1530,
	MONTH = dec,
	YEAR = 1998,
	ADDRESS = {Madras, India}
}

@inproceedings{Couturier98:CAV,
	TITLE = {An Experiment in Parallelizing an Application Using
		Formal Methods},
	AUTHOR = {Rapha\"{e}l Couturier and Dominique M\'{e}ry},
	BOOKTITLE = {Computer-Aided Verification, CAV '98},
	EDITOR = {Alan J. Hu and Moshe Y. Vardi},
	PAGES = {345--356},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1427,
	MONTH = jun,
	YEAR = 1998,
	ADDRESS = {Vancouver, Canada}
}

@inproceedings{Chkliaev99,
	TITLE = {Mechanical Verification of a Non-Blocking Atomic Commitment
		Protocol},
	AUTHOR = {Dmitri Chkliaev and Jozef Hooman and Peter van der
		Stok},
	BOOKTITLE = {International Workshop on Distributed System Validation
		and Verification (DSVV'2000)},
	PAGES = {E96--E103},
	MONTH = apr,
	YEAR = 2000,
	ADDRESS = {Taipei, Taiwan}
}

@inproceedings{Chkliaev99:AE,
	TITLE = {Serializability Preserving Extensions of Concurrency
		Control Protocols},
	AUTHOR = {Dmitri Chkliaev and Jozef Hooman and Peter van der
		Stok},
	BOOKTITLE = {Third International {Andrei Ershov} Memorial Conference:
		Perspectives of System Informatics, {PSI'99}},
	EDITOR = {D. Bj{\o}rner and M. Broy and A.V. Zamulin},
	PAGES = {180--193},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1755,
	MONTH = jul,
	YEAR = 1999,
	ADDRESS = {Novosibirsk, Russia}
}

@inproceedings{Chkliaev00:ICFEM,
	TITLE = {Mechanical Verification of Transaction Processing Systems},
	AUTHOR = {Dmitri Chkliaev and Jozef Hooman and Peter van der
		Stok},
	BOOKTITLE = {Third International Conference on Formal Engineering
		Methods (ICFEM 2000)},
	PAGES = {89--97},
	MONTH = nov,
	YEAR = 200,
	ORGANIZATION = {IEEE Computer Society},
	ADDRESS = {York, England}
}

@inproceedings{Couturier98:IFMW,
	TITLE = {Formal Engineering of the Bitonic Sort using {PVS}},
	AUTHOR = {Rapha\"{e}l Couturier},
	BOOKTITLE = {Proceedings, 2nd. Irish Workshop in Formal Methods},
	PUBLISHER = {Electronic Workshops in Computing (\url{http://ewic.org.uk/ewic/})},
	MONTH = jul,
	YEAR = 1998,
	ADDRESS = {Cork, Ireland}
}

@article{Devillers00:FMSD,
	TITLE = {Verification of a Leader Election Protocol: Formal Methods
		Applied to {IEEE 1394}},
	AUTHOR = {Marco Devillers and David Griffioen and Judi Romijn
		and Frits Vaandrager},
	JOURNAL = {Formal Methods in Systems Design},
	PAGES = {307--320},
	VOLUME = 16,
	NUMBER = 3,
	MONTH = jun,
	YEAR = 2000
}

@inproceedings{Glusman&Katz:CAV99,
	TITLE = {Mechanizing Proofs of Computation Equivalence},
	AUTHOR = {Marcelo Glusman and Shmuel Katz},
	BOOKTITLE = {Computer-Aided Verification, CAV '99},
	EDITOR = {Nicolas Halbwachs and Doron Peled},
	PAGES = {354--367},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1633,
	MONTH = jul,
	YEAR = 1999,
	ADDRESS = {Trento, Italy}
}

@inproceedings{Havelund:FMPPTA99,
	TITLE = {Mechanical Verification of a Garbage Collector},
	AUTHOR = {Klaus Havelund},
	BOOKTITLE = {Parallel and Distributed Processing (Combined Proceedings
		of 11 Workshops)},
	EDITOR = {Jos\'{e} Rolim and others},
	PAGES = {1258--1283},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1586,
	MONTH = apr,
	YEAR = 1999,
	ADDRESS = {San Juan, Puerto Rico},
	NOTE = {Presented at the Workshop on Formal Methods for Parallel
		Programming: Theory and Applications {(FMPPTA)}}
}

@article{Hooman98:EAS,
	TITLE = {Formal Verification of the Binary Exponential Backoff
		Protocol},
	AUTHOR = {Jozef Hooman},
	JOURNAL = {Proceedings of the Estonian Academy of Sciences (Special
		issue on the 9th Nordic Workshop on Programming Theory)},
	PAGES = {89--105},
	VOLUME = 4,
	NUMBER = 2,
	YEAR = 1998,
	NOTE = {Also available at \url{http://www.win.tue.nl/cs/tt/hooman/BEB.html}}
}

@inproceedings{Jackson98:tphols,
	TITLE = {Verifying a Garbage Collection Algorithm},
	AUTHOR = {Paul Jackson},
	BOOKTITLE = {Theorem Proving in Higher Order Logics: 11th International
		Conference, {TPHOLs '98}},
	EDITOR = {Jim Grundy and Malcolm Newey},
	PAGES = {225--244},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1479,
	MONTH = sep,
	YEAR = 1998,
	ADDRESS = {Canberra, Australia}
}

@article{Mokkedem00:FMSD,
	TITLE = {Formalization and Analysis of a Solution to the {PCI}
		2.1 Bus Transaction Ordering Problem},
	AUTHOR = {Abdel Mokkedem and Ravi M. Hosabettu and Michael D.
		Jones and Ganesh C. Gopalakrishnan},
	JOURNAL = {Formal Methods in Systems Design},
	PAGES = {93--119},
	VOLUME = 16,
	NUMBER = 1,
	MONTH = jan,
	YEAR = 2000
}

@inproceedings{Penix98:fmsp,
	TITLE = {Experiences in Verifying Parallel Simulation Algorithms},
	AUTHOR = {John Penix and Dale Martin and Peter Frey and Radharamanan
		Radhakrishnan and Perry Alexander and Phillip A. Wilsey},
	BOOKTITLE = {Second Workshop on Formal Methods in Software Practice
		(FMSP '98)},
	EDITOR = {Mark Ardis},
	PAGES = {16--23},
	MONTH = mar,
	YEAR = 1998,
	ORGANIZATION = {Association for Computing Machinery},
	ADDRESS = {Clearwater Beach, FL}
}

@article{Umamageswaran98:JSA,
	TITLE = {Formal Verification and Empirical Analysis of Rollback
		Relaxation},
	AUTHOR = {Kothanda Umamageswaran and Krishnan Subramani and Philip
		A. Wilsey and Perry Alexander},
	JOURNAL = {Journal of Systems Architecture (formerly published
		as Microprocessing and Microprogramming: the Euromicro
		Journal)},
	PAGES = {473--495},
	VOLUME = 44,
	NUMBER = {6--7},
	MONTH = mar,
	YEAR = 1998
}

@inproceedings{Alagar-etal99:RTAS,
	TITLE = {From Behavioral Specification to Axiomatic Description
		of Real-Time Reactive Systems},
	AUTHOR = {V. S. Alagar and D. Muthiayen and F. Pompeo},
	BOOKTITLE = {Fifth IEEE Real-Time Technology and Applications
		Symposium, Work-In-Progress Session},
	MONTH = jun,
	YEAR = 1999,
	ORGANIZATION = {IEEE Computer Society},
	ADDRESS = {Vancouver, British Columbia, Canada},
	NOTE = {Available at \url{http://www.cs.concordia.ca/~faculty/manas/rtas99wip/}}
}

@inproceedings{Alborghetti97:FSE,
	TITLE = {Providing Automated Support to Deductive Analysis of
		Time Critical Systems},
	AUTHOR = {Andren Alborghetti and Angelo Gargantini and Angelo
		Morzenti},
	BOOKTITLE = {Software Engineering---ESEC/FSE '97: Sixth European
		Software Engineering Conference and Fifth ACM SIGSOFT
		Symposium on the Foundations of Software Engineering},
	EDITOR = {Mehdi Jazayeri and Helmut Schauer},
	PAGES = {211--226},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1301,
	MONTH = sep,
	YEAR = 1997,
	ADDRESS = {Zurich, Switzerland}
}

@inproceedings{Archer&Heitmeyer96,
	TITLE = {Mechanical Verification of Timed Automata: A Case Study},
	AUTHOR = {Myla Archer and Constance Heitmeyer},
	BOOKTITLE = {IEEE Real-Time Technology and Applications Symposium
		(RTAS'96)},
	PAGES = {192--203},
	PUBLISHER = {IEEE Computer Society},
	MONTH = jun,
	YEAR = 1996,
	ADDRESS = {Brookline, MA}
}

@inproceedings{AHrtssWIP96,
	TITLE = {{TAME}: A Specialized Specification and Verification
		System for Timed Automata},
	AUTHOR = {M. Archer and C. Heitmeyer},
	BOOKTITLE = {Work In Progress (WIP) Proceedings of the 17th IEEE
		Real-Time Systems Symposium (RTSS'96)},
	EDITOR = {Azer Bestavros},
	PAGES = {3--6},
	MONTH = dec,
	YEAR = 1996,
	ADDRESS = {Washington, DC},
	NOTE = {The WIP Proceedings is available at \url{http://www.cs.bu.edu/pub/ieee-rts/rtss96/wip/proceedings}}
}

@inproceedings{Bun96:ASCI,
	TITLE = {Checking Properties of {ASTRAL} Specifications with
		{PVS}},
	AUTHOR = {Leon Bun},
	BOOKTITLE = {Proceedings of 2nd Annual Conference of the Advanced
		School for Computing and Imaging {(ASCI'96)}},
	PAGES = {102--107},
	MONTH = jun,
	YEAR = 1996,
	ADDRESS = {Lommel, Belgium},
	NOTE = {Available at \url{http://sepc.twi.tudelft.nl/~leonbun/papers/asci96.ps}}
}

@inproceedings{Bun97:ASCI,
	TITLE = {Embedding {Astral} in {PVS}},
	AUTHOR = {Leon Bun},
	BOOKTITLE = {Proceedings of 3rd Annual Conference of the Advanced
		School for Computing and Imaging {(ASCI'97)}},
	PAGES = {130--136},
	MONTH = jun,
	YEAR = 1997,
	ADDRESS = {Lommel, Belgium},
	NOTE = {Available at \url{http://sepc.twi.tudelft.nl/~leonbun/papers/asci97.ps}}
}

@inproceedings{deBoer96:ftrtft,
	TITLE = {Compositionality in Real-Time Shared Variable Concurrency},
	AUTHOR = {F. S. de Boer and H. Tej and W.-P. de Roever and M.
		van Hulst},
	BOOKTITLE = {Formal Techniques in Real-Time and Fault-Tolerant
		Systems},
	EDITOR = {Bengt Jonsson and Joachim Parrow},
	PAGES = {420--439},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1135,
	MONTH = sep,
	YEAR = 1996,
	ADDRESS = {Uppsala, Sweden}
}

@inproceedings{DuBois97:isre,
	TITLE = {On the Use of a Formal {RE} Language: The Generalized
		Railroad Crossing Problem},
	AUTHOR = {Philippe Du Bois and Eric Dubois and Jean-Marc Zeippen},
	BOOKTITLE = {3rd IEEE International Symposium on Requirements
		Engineering},
	PAGES = {128--137},
	MONTH = jan,
	YEAR = 1997,
	ORGANIZATION = {IEEE Computer Society},
	ADDRESS = {Annapolis, MD}
}

@techreport{dutertre99b,
	TITLE = {The {Priority Ceiling Protocol}: Formalization and Analysis
		Using {PVS}},
	AUTHOR = {Bruno Dutertre},
	MONTH = oct,
	YEAR = 1999,
	INSTITUTION = {System Design Laboratory, SRI International},
	ADDRESS = {Menlo Park, CA},
	NOTE = {Available at \url{http://www.sdl.sri.com/dsa/publis/prio-ceiling.html}}
}

@inproceedings{Dutertre&Stavridou00:DASC,
	TITLE = {Formal Analysis for Realtime Scheduling},
	AUTHOR = {Bruno Dutertre and Victoria Stavridou},
	BOOKTITLE = {19th AIAA/IEEE Digital Avionics Systems Conference},
	MONTH = oct,
	YEAR = 2000,
	ADDRESS = {Philadelphia, PA}
}

@inproceedings{Dutertre00:RTSS,
	TITLE = {Formal Analysis of the Priority Ceiling Protocol},
	AUTHOR = {Bruno Dutertre},
	BOOKTITLE = {Real Time Systems Symposium},
	MONTH = dec,
	YEAR = 2000,
	ORGANIZATION = {IEEE Computer Society},
	ADDRESS = {Orlando, FL},
	NOTE = {To appear}
}

@inproceedings{Fowler&Wellings96,
	TITLE = {Formal Analysis of a Real-Time Kernel Specification},
	AUTHOR = {Simon Fowler and Andy Wellings},
	BOOKTITLE = {Formal Techniques in Real-Time and Fault-Tolerant
		Systems},
	EDITOR = {Bengt Jonsson and Joachim Parrow},
	PAGES = {440--458},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1135,
	MONTH = sep,
	YEAR = 1996,
	ADDRESS = {Uppsala, Sweden}
}

@inproceedings{Fowler97:RTSS,
	TITLE = {Formal Development Of A Real-Time Kernel},
	AUTHOR = {Simon Fowler and Andy Wellings},
	BOOKTITLE = {Real Time Systems Symposium},
	PAGES = {220--229},
	MONTH = dec,
	YEAR = 1997,
	ORGANIZATION = {IEEE Computer Society},
	ADDRESS = {San Francisco, CA}
}

@inproceedings{Hooman94,
	TITLE = {Correctness of Real Time Systems by Construction},
	AUTHOR = {Jozef Hooman},
	BOOKTITLE = {Formal Techniques in Real-Time and Fault-Tolerant
		Systems},
	EDITOR = {H. Langmaack and W.-P. {de Roever} and J. Vytopil},
	PAGES = {19--40},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 863,
	MONTH = sep,
	YEAR = 1994,
	ADDRESS = {L\"{u}beck, Germany}
}

@inproceedings{Hooman96:RPC,
	TITLE = {Using {PVS} for an Assertional Verification of the {RPC-Memory}
		Specification Problem},
	AUTHOR = {Jozef Hooman},
	BOOKTITLE = {Formal Systems Specification: The {RPC-Memory} Specification
		Case Study},
	EDITOR = {Manfred Broy and Stephan Merz and Katharina Spies},
	PAGES = {275--304},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1169,
	YEAR = 1996
}

@inproceedings{Hooman97:AMAST,
	TITLE = {Verification of Distributed Real-Time and Fault-Tolerant
		Protocols},
	AUTHOR = {Jozef Hooman},
	BOOKTITLE = {Algebraic Methodology and Software Technology, {AMAST}'97},
	EDITOR = {Michael Johnson},
	PAGES = {261--275},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1349,
	MONTH = dec,
	YEAR = 1997,
	ADDRESS = {Sydney, Australia}
}

@inproceedings{Hooman97:compos,
	TITLE = {Compositional Verification of Real-Time Applications},
	AUTHOR = {Jozef Hooman},
	BOOKTITLE = {Compositionality: The Significant Difference (Revised
		lectures from International Symposium {COMPOS'97})},
	EDITOR = {Willem-Paul de Roever and Hans Langmaack and Amir Pnueli},
	PAGES = {276--300},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1536,
	MONTH = sep,
	YEAR = 1997,
	ADDRESS = {Bad Malente, Germany}
}

@inproceedings{Kolano99:ARTS,
	TITLE = {Proof Assistance for Real-Time Systems Using an Interactive
		Theorem Prover},
	AUTHOR = {Paul Z. Kolano},
	BOOKTITLE = {Formal Methods for Real-Time and Probabilistic Systems
		(Proceedings 5th International {AMAST} Workshop, {ARTS'99})},
	EDITOR = {J.-P. Katoen},
	PAGES = {315--333},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1601,
	MONTH = may,
	YEAR = 1999,
	ADDRESS = {Bamberg, Germany}
}

@inproceedings{Kolano-etal00:FASE,
	TITLE = {Parallel Refinement Mechanisms for Real-Time Systems},
	AUTHOR = {Paul Kolano and Richard Kemmerer and Dino Mandrioli},
	BOOKTITLE = {Fundamental Approaches to Software Engineering,
		{FASE} 2000},
	EDITOR = {Tom Maibaum},
	PAGES = {35--50},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	NUMBER = 1783,
	MONTH = {March/April},
	YEAR = 2000,
	ADDRESS = {Berlin, Germany}
}

@phdthesis{Muthiayen00,
	TITLE = {Real-Time Reactive System Development---A Formal Approach
		Based on {UML} and {PVS}},
	AUTHOR = {Darmalingum Muthiayen},
	MONTH = jan,
	YEAR = 2000,
	SCHOOL = {Department of Computer Science at Concordia University},
	ADDRESS = {Montreal, Canada}
}

@inproceedings{Shankar93:CAV,
	TITLE = {Verification of Real-Time Systems Using {PVS}},
	AUTHOR = {Natarajan Shankar},
	BOOKTITLE = {Computer-Aided Verification, CAV '93},
	EDITOR = {Costas Courcoubetis},
	PAGES = {280--291},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 697,
	MONTH = {June/July},
	YEAR = 1993,
	ADDRESS = {Elounda, Greece}
}

@phdthesis{Skakkebaek94:thesis,
	TITLE = {A Verification Assistant for a Real-Time Logic},
	AUTHOR = {Jens Ulrik Skakkeb{\ae}k},
	MONTH = nov,
	YEAR = 1994,
	SCHOOL = {Department of Computer Science, Technical University
		of Denmark},
	ADDRESS = {Lyngby, Denmark}
}

@inproceedings{Skakkebaek&Shankar94,
	TITLE = {Towards a {Duration Calculus} Proof Assistant in {PVS}},
	AUTHOR = {Jens U. Skakkeb{\ae}k and N. Shankar},
	BOOKTITLE = {Formal Techniques in Real-Time and Fault-Tolerant
		Systems},
	EDITOR = {H. Langmaack and W.-P. {de Roever} and J. Vytopil},
	PAGES = {660--679},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 863,
	MONTH = sep,
	YEAR = 1994,
	ADDRESS = {L\"{u}beck, Germany}
}

@inproceedings{Kellomaki97,
	TITLE = {Verification of Reactive Systems Using {DisCo} and {PVS}},
	AUTHOR = {Pertti Kellom\"{a}ki},
	BOOKTITLE = {Formal Methods Europe {FME '97}},
	PAGES = {589--604},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1313,
	MONTH = sep,
	YEAR = 1997,
	ADDRESS = {Graz, Austria}
}

@inproceedings{AHhart97,
	TITLE = {Verifying Hybrid Systems Modeled as Timed Automata:
		A Case Study},
	AUTHOR = {M. Archer and C. Heitmeyer},
	BOOKTITLE = {Proceedings of the International Workshop on Hybrid
		and Real-Time Systems (HART'97)},
	EDITOR = {Oded Maler},
	PAGES = {171--185},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1201,
	MONTH = mar,
	YEAR = 1997,
	ADDRESS = {Grenoble, France}
}

@inproceedings{Henzinger&Rusu98,
	TITLE = {Reachability Verification for Hybrid Automata},
	AUTHOR = {Thomas A. Henzinger and Vlad Rusu},
	BOOKTITLE = {Hybrid Systems: Computation and Control (First International
		Workshop, {HSCC'98})},
	EDITOR = {Thomas A. Henzinger and Shankar Sastry},
	PAGES = {190--204},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1386,
	MONTH = apr,
	YEAR = 1998,
	ADDRESS = {Berkeley, CA}
}

@inproceedings{Hooman96:boiler,
	TITLE = {Assertional Specification and Verification Using {PVS}
		of the Steam Boiler Control System},
	AUTHOR = {Jan Vitt and Jozef Hooman},
	BOOKTITLE = {Formal Methods for Industrial Applications: Specifying
		and Programming the Steam Boiler Control},
	EDITOR = {Jean-Raymond Abrial and Egon Boerger and Hans Langmaack},
	PAGES = {453--472},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1165,
	YEAR = 1996
}

@inproceedings{Bloo-etal00:SAC,
	TITLE = {Semantical Aspects of an Architecture for Distributed
		Embedded Systems},
	AUTHOR = {Roel Bloo and Jozef Hooman and Edwin de Jong},
	BOOKTITLE = {Proceedings of the 2000 ACM Symposium on Applied
		Computing {(SAC 2000)}},
	PAGES = {149-155},
	VOLUME = 1,
	MONTH = mar,
	YEAR = 2000,
	ORGANIZATION = {Association for Computing Machinery},
	ADDRESS = {Como, Italy}
}

@inproceedings{deJong00:ECBS,
	TITLE = {Refinement in Requirements Specification and Analysis:
		A Case Study},
	AUTHOR = {Edwin de Jong and Jaco van de Pol and Jozef Hooman},
	BOOKTITLE = {7th IEEE International Conference and Workshop on
		the Engineering of Computer Based Systems {(ECBS)}},
	PAGES = {290--298},
	MONTH = apr,
	YEAR = 2000,
	ORGANIZATION = {IEEE Computer Society},
	ADDRESS = {Edinburgh, Scotland}
}

@inproceedings{vandePol-etal99:IFM,
	TITLE = {Modular Formal Specification of Data and Behaviour},
	AUTHOR = {Jaco van de Pol and Jozef Hooman and Edwin de Jong},
	BOOKTITLE = {Proceedings 1st Conference on Integrated Formal
		Methods {(IFM'99)}},
	EDITOR = {K. Araki and A. Galloway and K. Taguchi},
	PAGES = {109--128},
	PUBLISHER = {Springer},
	MONTH = jun,
	YEAR = 1999,
	ADDRESS = {York, UK}
}

@inproceedings{deBoer&Hulst96,
	TITLE = {Local Nondeterminism in Asynchronously Communicating
		Processes},
	AUTHOR = {Frank S. de Boer and Marten van Hulst},
	BOOKTITLE = {Formal Methods Europe {FME '96}},
	PAGES = {367--384},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1051,
	MONTH = mar,
	YEAR = 1996,
	ADDRESS = {Oxford, UK}
}

@inproceedings{Chernyskhovsky:FMPPTA99,
	TITLE = {A Formal Framework for Specifying and Verifying Time
		Warp Optimizations},
	AUTHOR = {Victoria Chernyakhovsky and Peter Frey and Radharamanan
		Radhakrihnan and Philip A. Wilsey and Perry Alexander
		and Harold W. Carter},
	BOOKTITLE = {Parallel and Distributed Processing (Combined Proceedings
		of 11 Workshops)},
	EDITOR = {Jos\'{e} Rolim and others},
	PAGES = {1228--1242},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1586,
	MONTH = apr,
	YEAR = 1999,
	ADDRESS = {San Juan, Puerto Rico},
	NOTE = {Presented at the Workshop on Formal Methods for Parallel
		Programming: Theory and Applications {(FMPPTA)}}
}

@inproceedings{Frey99:HICSS,
	TITLE = {An Extensible Formal Framework for the Specification
		and Verification of an Optimistic Simulation Protocol},
	AUTHOR = {Peter Frey and Radharamanan Radhakrishnan and Philip
		A. Wilsey and Perry Alexander and Harold W. Carter},
	BOOKTITLE = {Proceedings of the 32nd Annual Hawaii International
		Conference on System Sciences},
	MONTH = jan,
	YEAR = 1999,
	ORGANIZATION = {IEEE Computer Society},
	NOTE = {Available at \url{http://computer.org/conferen/proceed/hicss/0001/00013/00013049abs.htm}}
}

@inproceedings{Hooman98:TOOLS96,
	TITLE = {Developing Proof Rules for Distributed Real-Time Systems
		with {PVS}},
	AUTHOR = {Jozef Hooman},
	BOOKTITLE = {Tools for System Development and Verification},
	EDITOR = {Bettina Buth and Rudolf Berghammer and Jan Peleska},
	PAGES = {120--139},
	PUBLISHER = {Shaker Verlag},
	SERIES = {BISS Monographs},
	YEAR = 1998,
	ADDRESS = {Aachen, Germany},
	NOTE = {Proceedings of a workshop held at Bremen in 1996}
}

@inproceedings{Kellomaki95,
	TITLE = {Mechanizing Invariant Proofs of Joint Action Systems},
	AUTHOR = {Pertti Kellom\"{a}ki},
	BOOKTITLE = {Fourth Symposium on Programming Languages and Software
		Tools},
	PAGES = {141--152},
	MONTH = jun,
	YEAR = 1995,
	ADDRESS = {Visegrad, Hungary},
	NOTE = {Available at \url{http://www.cs.tut.fi/~pk/papers/visegrad-95/visegrad.ps.gz}}
}

@inproceedings{Kellomaki96:tphols,
	TITLE = {Using Auxiliary Knowledge in Automating Invariant Proofs},
	AUTHOR = {Pertti Kellom\"{a}ki},
	BOOKTITLE = {International Conference on Theorem Proving in Higher
		Order Logics},
	PAGES = {57--68},
	MONTH = aug,
	YEAR = 1996,
	ADDRESS = {Turku, Finland},
	NOTE = {Supplementary proceedings, available at \url{http://www.tucs.abo.fi/publications/general/G1.html}}
}

@inproceedings{Lesens&Saidi97,
	TITLE = {Automatic Verification of Parameterized Networks of
		Processes by Abstraction},
	AUTHOR = {David Lesens and Hassen Sa{\"\i}di},
	BOOKTITLE = {2nd International Workshop on Verification of Infinite
		State Systems: Infinity '97},
	EDITOR = {Faron Moller},
	PUBLISHER = {Elsevier},
	SERIES = {Electronic Notes in Theoretical Computer Science},
	VOLUME = 9,
	MONTH = jul,
	YEAR = 1997,
	ADDRESS = {Bologna, Italy},
	NOTE = {Available at \url{http://www.elsevier.nl/cas/tree/store/tcs/free/entcs/store/tcs9/tcs9009%
		.ps}}
}

@techreport{Shankar93:lazy,
	TITLE = {A Lazy Approach to Compositional Verification},
	AUTHOR = {N. Shankar},
	NUMBER = {SRI-CSL-93-8},
	MONTH = dec,
	YEAR = 1993,
	INSTITUTION = {Computer Science Laboratory, SRI International},
	ADDRESS = {Menlo Park, CA}
}

@phdthesis{vanHulst:thesis,
	TITLE = {Compositional Verification of Parallel Programs using
		Epistemic Logic and Abstract Assertional Languages},
	AUTHOR = {Marten van Hulst},
	MONTH = jun,
	YEAR = 1995,
	SCHOOL = {Faculteit Wiskunde en Informatica, Universiteit Utrecht},
	ADDRESS = {The Netherlands}
}

@inproceedings{Hooman95,
	TITLE = {Verifying Part of the {ACCESS.bus} Protocol Using {PVS}},
	AUTHOR = {Jozef Hooman},
	BOOKTITLE = {15th Conference on the Foundations of Software Technology
		and Theoretical Computer Science},
	EDITOR = {P. S. Thiagarajan},
	PAGES = {96--110},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1026,
	MONTH = dec,
	YEAR = 1995,
	ADDRESS = {Bangalore, India}
}

@inproceedings{Havelund&Shankar96,
	TITLE = {Experiments in Theorem Proving and Model Checking for
		Protocol Verification},
	AUTHOR = {Klaus Havelund and N. Shankar},
	BOOKTITLE = {Formal Methods Europe {FME '96}},
	PAGES = {662--681},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1051,
	MONTH = mar,
	YEAR = 1996,
	ADDRESS = {Oxford, UK}
}

@inproceedings{Khune-etal97,
	TITLE = {Towards Mechanical Verification of Parts of the {IEEE
		P1394} Serial Bus},
	AUTHOR = {Lars Kh\"{u}ne and Jozef Hooman and Willem-Paul de
		Roever},
	BOOKTITLE = {2nd International Workshop on Applied Formal Methods
		in System Design},
	MONTH = jun,
	YEAR = 1997,
	ADDRESS = {Zagreb, Croatia},
	NOTE = {Available at \url{http://www.win.tue.nl/cs/tt/hooman/P1394.html}}
}

@inproceedings{Mokkedem&Leonard00:TPHOLS,
	TITLE = {Formal Verification of the {Alpha} 21364 Network Protocol},
	AUTHOR = {Abdel Mokkedem and Tim Leonard},
	BOOKTITLE = {Theorem Proving in Higher Order Logics: 13th International
		Conference, {TPHOLs 2000}},
	EDITOR = {Mark Aargaard and John Harrison},
	PAGES = {443--461},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1869,
	MONTH = aug,
	YEAR = 2000,
	ADDRESS = {Portland, OR}
}

@inproceedings{Rusinowitch-etal00:CAV,
	TITLE = {Mechanical Verification of a Generic Incremental {ABR}
		Conformance Algorithm},
	AUTHOR = {Micha\"{e}l Rusinowitch and Sorin Stratulat and Francis
		Klay},
	BOOKTITLE = {Computer-Aided Verification, CAV '2000},
	EDITOR = {E. A. Emerson and A. P. Sistla},
	PAGES = {344--357},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1855,
	MONTH = jul,
	YEAR = 2000,
	ADDRESS = {Chicago, IL}
}

@inproceedings{Herbert-etal:FM99,
	TITLE = {A Formalization of Software Architecture},
	AUTHOR = {John Herbert and Bruno Dutertre and Robert Riemenschneider
		and Victoria Stavridou},
	BOOKTITLE = {FM99: The World Congress in Formal Methods},
	EDITOR = {Jeannette Wing and Jim Woodcock},
	PAGES = {116--133},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = {1708 and 1709},
	MONTH = sep,
	YEAR = 1999,
	ADDRESS = {Toulouse, France},
	NOTE = {Pages 1--938 are in the first volume, 939--1872 in the
		second.}
}

@inproceedings{Hooman97,
	TITLE = {Program Design in {PVS}},
	AUTHOR = {Jozef Hooman},
	BOOKTITLE = {Workshop on Tool Support for System Development
		and Verification},
	EDITOR = {K.Berghammer and J.Peleska and B. Buth},
	YEAR = 1997,
	ADDRESS = {Bremen, Germany},
	NOTE = {Available at \url{http://www.win.tue.nl/cs/tt/hooman/PDPVS.html}}
}

@inproceedings{Levy&Trilling:FM99,
	TITLE = {A {PVS}-Based Approach for Teaching Constructing Correct
		Iterations},
	AUTHOR = {Michel L\'{e}vy and Laurent Trilling},
	BOOKTITLE = {FM99: The World Congress in Formal Methods},
	EDITOR = {Jeannette Wing and Jim Woodcock},
	PAGES = {1859--1860},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = {1708 and 1709},
	MONTH = sep,
	YEAR = 1999,
	ADDRESS = {Toulouse, France},
	NOTE = {Pages 1--938 are in the first volume, 939--1872 in the
		second.}
}

@inproceedings{Verhoeven&Backhouse:FM99,
	TITLE = {Interfacing Program Construction and Verification},
	AUTHOR = {Richard Verhoeven and Roland Backhouse},
	BOOKTITLE = {FM99: The World Congress in Formal Methods},
	EDITOR = {Jeannette Wing and Jim Woodcock},
	PAGES = {1128--1146},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = {1708 and 1709},
	MONTH = sep,
	YEAR = 1999,
	ADDRESS = {Toulouse, France},
	NOTE = {Pages 1--938 are in the first volume, 939--1872 in the
		second.}
}

@inproceedings{Behnke98:TOOLS96,
	TITLE = {Supporting Algebraic Program Derivation by {PVS}},
	AUTHOR = {Ralf Behnke and Rudolf Berghammer and S\"{o}nke Magnussen},
	BOOKTITLE = {Tools for System Development and Verification},
	EDITOR = {Bettina Buth and Rudolf Berghammer and Jan Peleska},
	PAGES = {22--40},
	PUBLISHER = {Shaker Verlag},
	SERIES = {BISS Monographs},
	YEAR = 1998,
	ADDRESS = {Aachen, Germany},
	NOTE = {Proceedings of a workshop held at Bremen in 1996}
}

@inproceedings{Dold95,
	TITLE = {Representing, Verifying and Applying Software Development
		Steps using the {PVS} system},
	AUTHOR = {Axel Dold},
	BOOKTITLE = {Algebraic Methodology and Software Technology, AMAST'95},
	EDITOR = {V. S. Alagar and Maurice Nivat},
	PAGES = {431--445},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 936,
	MONTH = jul,
	YEAR = 1995,
	ADDRESS = {Montreal, Canada}
}

@phdthesis{Dold:PhD,
	TITLE = {Formal Software Development using Generic Development
		Steps},
	AUTHOR = {Axel Dold},
	YEAR = 2000,
	SCHOOL = {Universit{\"a}t Ulm, Germany}
}

@inproceedings{Shankar:MPC95,
	TITLE = {Computer-Aided Computing},
	AUTHOR = {N. Shankar},
	BOOKTITLE = {Mathematics of Program Construction '95},
	EDITOR = {Bernhard M\"oller},
	PAGES = {50--66},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 947,
	YEAR = 1995
}

@article{Shankar:SCP96,
	TITLE = {Steps Towards Mechanizing Program Transformations Using
		{PVS}},
	AUTHOR = {N. Shankar},
	JOURNAL = {Science of Computer Programming},
	PAGES = {33--57},
	VOLUME = 26,
	NUMBER = {1--3},
	YEAR = 1996
}

@inproceedings{Jacobs97,
	TITLE = {Behaviour-Refinement of Coalgebraic Specifications with
		Coinductive Correctness Proofs},
	AUTHOR = {Bart Jacobs},
	BOOKTITLE = {{TAPSOFT} '97: Theory and Practice of Software Development},
	EDITOR = {Michel Bidoit and Max Dauchet},
	PAGES = {787--802},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1214,
	MONTH = apr,
	YEAR = 1997,
	ADDRESS = {Lille, France}
}

@inproceedings{Jacobs97:AMAST,
	TITLE = {Invariants, Bisimulations and the Correctness of Coalgebraic
		Refinements},
	AUTHOR = {Bart Jacobs},
	BOOKTITLE = {Algebraic Methodology and Software Technology, {AMAST}'97},
	EDITOR = {Michael Johnson},
	PAGES = {276--291},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1349,
	MONTH = dec,
	YEAR = 1997,
	ADDRESS = {Sydney, Australia}
}

@inproceedings{Jackson00:TPHOLS,
	TITLE = {Total-Correctness Refinement for Sequential Reactive
		Systems},
	AUTHOR = {Paul Jackson},
	BOOKTITLE = {Theorem Proving in Higher Order Logics: 13th International
		Conference, {TPHOLs 2000}},
	EDITOR = {Mark Aargaard and John Harrison},
	PAGES = {320--337},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1869,
	MONTH = aug,
	YEAR = 2000,
	ADDRESS = {Portland, OR}
}

@mastersthesis{Knappmann96,
	TITLE = {A {PVS} Based Tool for Developing Programs in the {Refinement
		Calculus}},
	AUTHOR = {Jens Knappmann},
	MONTH = oct,
	YEAR = 1996,
	SCHOOL = {Institut f\"{u}r Informatik und Praktische Mathematik
		der Christian-Albrechts-Universit\"{a}t zu Kiel},
	ADDRESS = {Kiel, Germany}
}

@techreport{K-HButh95,
	TITLE = {Automated Code Generator Verification Based on Algebraic
		Laws},
	AUTHOR = {Karl-Heinz Buth},
	TYPE = {Procos II Report},
	NUMBER = {Kiel KHB 5/1},
	MONTH = sep,
	YEAR = 1995,
	INSTITUTION = {Christian-Albrechts Universit{\"a}t zu Kiel},
	ADDRESS = {Kiel, Germany},
	NOTE = {Available at \url{ftp://ftp.informatik.uni-kiel.de/pub/kiel/procos/kiel-khb-5-1.ps.Z}}
}

@inproceedings{Dold-etal97,
	TITLE = {Formal Verification of Transformations for Peephole
		Optimiztion},
	AUTHOR = {A. Dold and F. W. von Henke and H. Pfeifer and H. Rue{\ss}},
	BOOKTITLE = {Formal Methods Europe {FME '97}},
	PAGES = {459--472},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1313,
	MONTH = sep,
	YEAR = 1997,
	ADDRESS = {Graz, Austria}
}

@inproceedings{DGVZ98,
	TITLE = {{{ASM}-Based Mechanized Verification of Compiler Backends}},
	AUTHOR = {A. Dold and T. Gaul and V. Vialard and W. Zimmermann},
	BOOKTITLE = {Proceedings of the 5th International Workshop on
		Abstract State Machines},
	EDITOR = {Uwe Gl{\"a}sser and Peter H. Schmitt},
	PAGES = {50-67},
	MONTH = sep,
	YEAR = 1998,
	ADDRESS = {Magdeburg, Germany},
	NOTE = {Available at \url{http://i44www.info.uni-karlsruhe.de/~verifix/pres/paper/ASM-WS98-DGVZ.p%
		s.gz}}
}

@inproceedings{Dold-etal98:STTT,
	TITLE = {Mechanized Verification of Compiler Backends},
	AUTHOR = {Axel Dold and Thilo Gaul and Wolf Zimmermann},
	BOOKTITLE = {Proceedings of the International Workshop on Software
		Tools for Technology Transfer {STTT'98}},
	EDITOR = {Tiziana Margaria and Bernhard Steffen},
	PAGES = {13--22},
	MONTH = jun,
	YEAR = 1998,
	ORGANIZATION = {BRICS NS-98-4},
	ADDRESS = {Aalborg, Denmark},
	NOTE = {Proceedings available at \url{http://www.brics.dk/NS/98/4/}}
}

@inproceedings{Dold&Vialard99,
	TITLE = {Formal Verification of a Compiler Back-End Generic Checker
		Program},
	AUTHOR = {Axel Dold and Vincent Vialard},
	BOOKTITLE = {Third International {Andrei Ershov} Memorial Conference:
		Perspectives of System Informatics, {PSI'99}},
	EDITOR = {D. Bj{\o}rner and M. Broy and A.V. Zamulin},
	PAGES = {470--480},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1755,
	MONTH = jul,
	YEAR = 1999,
	ADDRESS = {Novosibirsk, Russia}
}

@inproceedings{Stringer-Calvert97,
	TITLE = {Using {PVS} to Prove a {Z} refinement: A Case Study},
	AUTHOR = {David W. J. Stringer-Calvert and Susan Stepney and
		Ian Wand},
	BOOKTITLE = {Formal Methods Europe {FME '97}},
	PAGES = {573--588},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1313,
	MONTH = sep,
	YEAR = 1997,
	ADDRESS = {Graz, Austria}
}

@phdthesis{Stringer-Calvert98:thesis,
	TITLE = {Mechanical Verification of Compiler Correctness},
	AUTHOR = {David W. J. Stringer-Calvert},
	MONTH = mar,
	YEAR = 1998,
	SCHOOL = {University of York, Department of Computer Science},
	ADDRESS = {York, England},
	NOTE = {Available at \url{http://www.csl.sri.com/~dave_sc/papers/thesis.html}}
}

@techreport{Wahab:UWARWICK:CS-RR-354,
	TITLE = {Verification and Abstraction of Flow-Graph Programs
		with Pointers and Computed Jumps},
	AUTHOR = {M. Wahab},
	TYPE = {Research Report},
	NUMBER = {CS-RR-354},
	MONTH = nov,
	YEAR = 1998,
	INSTITUTION = {Department of Computer Science, University of
		Warwick},
	ADDRESS = {Coventry, UK},
	NOTE = {Available at \url{http://www.dcs.warwick.ac.uk/pub/reports/rr/354.html}}
}

@phdthesis{Wahab98,
	TITLE = {Object Code Verification},
	AUTHOR = {Matthew Wahab},
	MONTH = dec,
	YEAR = 1998,
	SCHOOL = {Department of Computer Science, University of Warwick},
	ADDRESS = {Coventry, UK},
	NOTE = {Available at \url{http://www.dcs.warwick.ac.uk/pub/reports/theses/wahab98.html}}
}

@inproceedings{Arons99:VLSI,
	TITLE = {Verifying {Tomasulo'}s Algorithm by Refinement},
	AUTHOR = {Tamara Arons and Amir Pnueli},
	BOOKTITLE = {The Twelfth International Conference on {VLSI} Design},
	PAGES = {306--309},
	MONTH = jan,
	YEAR = 1999,
	ORGANIZATION = {IEEE Computer Society},
	ADDRESS = {Goa, India}
}

@inproceedings{Arons&Pnueli00:TACAS,
	TITLE = {A Comparison of two Verification Methods for Speculative
		Instruction Execution},
	AUTHOR = {Tamarah Arons and Amir Pnueli},
	BOOKTITLE = {Tools and Algorithms for the Construction and Analysis
		of Systems {(TACAS 2000)}},
	EDITOR = {Susanne Graf and Michael Schwartzbach},
	PAGES = {487--502},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	NUMBER = 1785,
	MONTH = mar,
	YEAR = 2000,
	ADDRESS = {Berlin, Germany}
}

@inproceedings{Cyrluk96:FMCAD,
	TITLE = {Inverting the Abstraction Mapping: A Methodology for
		Hardware Verification},
	AUTHOR = {David Cyrluk},
	BOOKTITLE = {Formal Methods in Computer-Aided Design (FMCAD '96)},
	EDITOR = {Mandayam Srivas and Albert Camilleri},
	PAGES = {172--186},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1166,
	MONTH = nov,
	YEAR = 1996,
	ADDRESS = {Palo Alto, CA}
}

@inproceedings{Cyrluk97:ICFEM,
	TITLE = {Systematic Formal Verification of Interpreters},
	AUTHOR = {David Cyrluk and John Rushby and Mandayam Srivas},
	BOOKTITLE = {First International Conference on Formal Engineering
		Methods (ICFEM '97)},
	EDITOR = {Michael G. Hinchey and Shaoying Liu},
	PAGES = {140--149},
	MONTH = nov,
	YEAR = 1997,
	ORGANIZATION = {IEEE Computer Society},
	ADDRESS = {Hiroshima, Japan}
}

@inproceedings{Damm&Pnueli97,
	TITLE = {Verifying Out-of-Order Executions},
	AUTHOR = {Werner Damm and Amir Pnueli},
	BOOKTITLE = {Advances in Hardware Design and Verification: {IFIP
		WG10.5} International Conference on Correct Hardware
		Design and Verification Methods (CHARME)},
	EDITOR = {Hon F. li and David K. Probst},
	PAGES = {23--47},
	PUBLISHER = {Chapman \& Hall},
	MONTH = oct,
	YEAR = 1997,
	ADDRESS = {Montreal, Canada}
}

@inproceedings{Fisler94:TPCD,
	TITLE = {Extending Formal Reasoning with Support for Hardware
		Diagrams},
	AUTHOR = {Kathi Fisler},
	BOOKTITLE = {Theorem Provers in Circuit Design ({TPCD} '94)},
	EDITOR = {Ramayya Kumar and Thomas Kropf},
	PAGES = {298--303},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 910,
	MONTH = sep,
	YEAR = 1994,
	ADDRESS = {Bad Herrenalb, Germany}
}

@inproceedings{Gopalakrishnan-etal97,
	TITLE = {Formal Modeling and Validation Applied to a Commercial
		Coherent Bus: A Case Study},
	AUTHOR = {Ganesh Gopalakrishnan and Rajnish Ghughal and Ravi
		Hosabettu and Abdelillah Mokkedem and Ratan Nalumasu},
	BOOKTITLE = {Advances in Hardware Design and Verification: {IFIP
		WG10.5} International Conference on Correct Hardware
		Design and Verification Methods (CHARME)},
	EDITOR = {Hon F. li and David K. Probst},
	PAGES = {48--62},
	PUBLISHER = {Chapman \& Hall},
	MONTH = oct,
	YEAR = 1997,
	ADDRESS = {Montreal, Canada}
}

@inproceedings{Greve98:FMCAD,
	TITLE = {Symbolic Simulation of the {JEM1} Microprocessor},
	AUTHOR = {David Greve},
	BOOKTITLE = {Formal Methods in Computer-Aided Design (FMCAD '98)},
	EDITOR = {Ganesh Gopalakrishnan and Phillip Windley},
	PAGES = {321--333},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1522,
	MONTH = nov,
	YEAR = 1998,
	ADDRESS = {Palo Alto, CA}
}

@inproceedings{Hardin98:CAV,
	TITLE = {Transforming the Theorem Prover into a Digital Design
		Tool: From Concept Car to Off-Road Vehicle},
	AUTHOR = {David Hardin and Matthew Wilding and David Greve},
	BOOKTITLE = {Computer-Aided Verification, CAV '98},
	EDITOR = {Alan J. Hu and Moshe Y. Vardi},
	PAGES = {39--44},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1427,
	MONTH = jun,
	YEAR = 1998,
	ADDRESS = {Vancouver, Canada}
}

@inproceedings{Hosabettu98:CAV,
	TITLE = {Decomposing the Proof of Correctness of Pipelined Microprocessors},
	AUTHOR = {Ravi Hosabettu and Mandayam Srivas and Ganesh Gopalakrishnan},
	BOOKTITLE = {Computer-Aided Verification, CAV '98},
	EDITOR = {Alan J. Hu and Moshe Y. Vardi},
	PAGES = {122--134},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1427,
	MONTH = jun,
	YEAR = 1998,
	ADDRESS = {Vancouver, Canada}
}

@inproceedings{Hosabettu:CAV99,
	TITLE = {Proof of Correctness of a Processor with Reorder Buffer
		using the Completion Functions Approach},
	AUTHOR = {Ravi Hosabettu and Mandayam Srivas and Ganesh Gopalakrishnan},
	BOOKTITLE = {Computer-Aided Verification, CAV '99},
	EDITOR = {Nicolas Halbwachs and Doron Peled},
	PAGES = {47--59},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1633,
	MONTH = jul,
	YEAR = 1999,
	ADDRESS = {Trento, Italy}
}

@inproceedings{Hosabettu:CHARME99,
	TITLE = {Proof of Correctness of a Processor Implementing {Tomasulo's}
		Algorithm without a Reorder Buffer},
	AUTHOR = {Ravi Hosabettu and Ganesh Gopalakrishnan and Mandayam
		Srivas},
	BOOKTITLE = {Advances in Hardware Design and Verification: {IFIP
		WG10.5} International Conference on Correct Hardware
		Design and Verification Methods (CHARME '99)},
	PAGES = {8--22},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1703,
	MONTH = sep,
	YEAR = 1999,
	ADDRESS = {Bad Herrenalb, Germany}
}

@inproceedings{Hosabettu-etal00:CAV,
	TITLE = {Verifying Microarchitectures that Support Speculation
		and Exceptions},
	AUTHOR = {Ravi Hosabettu and Ganesh Gopalakrishnan and Mandayam
		Srivas},
	BOOKTITLE = {Computer-Aided Verification, CAV '2000},
	EDITOR = {E. A. Emerson and A. P. Sistla},
	PAGES = {521--537},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1855,
	MONTH = jul,
	YEAR = 2000,
	ADDRESS = {Chicago, IL}
}

@inproceedings{Johnson94:TPCD,
	TITLE = {Studies of the Single-Pulser in Various Reasoning Systems},
	AUTHOR = {Steven D. Johnson and Paul S. Miner and Albert Camlleri},
	BOOKTITLE = {Theorem Provers in Circuit Design ({TPCD} '94)},
	EDITOR = {Ramayya Kumar and Thomas Kropf},
	PAGES = {126--145},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 910,
	MONTH = sep,
	YEAR = 1994,
	ADDRESS = {Bad Herrenalb, Germany}
}

@inproceedings{Johnson&Miner97,
	TITLE = {Integrated Reasoning Support in System Design: Design
		Derivation and Theorem Proving},
	AUTHOR = {Steven D. Johnson and Paul S. Miner},
	BOOKTITLE = {Advances in Hardware Design and Verification: {IFIP
		WG10.5} International Conference on Correct Hardware
		Design and Verification Methods (CHARME)},
	EDITOR = {Hon F. li and David K. Probst},
	PAGES = {255--272},
	PUBLISHER = {Chapman \& Hall},
	MONTH = oct,
	YEAR = 1997,
	ADDRESS = {Montreal, Canada}
}

@inproceedings{Leathrum97:LFM,
	TITLE = {Fundamental Hardware Design in {PVS}},
	AUTHOR = {James {Leathrum, Jr.}},
	BOOKTITLE = {LFM' 97: Fourth NASA Langley Formal Methods Workshop},
	EDITOR = {C. Michael Holloway and Kelly J. Hayhurst},
	PAGES = {193--204},
	SERIES = {NASA Conference Publication 3356},
	MONTH = sep,
	YEAR = 1997,
	ORGANIZATION = {NASA Langley Research Center},
	ADDRESS = {Hampton, VA},
	NOTE = {Available at \url{http://atb-www.larc.nasa.gov/Lfm97/proceedings/}}
}

@inproceedings{Li-etal97,
	TITLE = {Proving the Correctness of the Interlock Mechanism in
		Processor Design},
	AUTHOR = {Xiaoshan Li and Antonio Cau and Ben Moszkowski and
		Nick Coleman and Hussein Zedan},
	BOOKTITLE = {Advances in Hardware Design and Verification: {IFIP
		WG10.5} International Conference on Correct Hardware
		Design and Verification Methods (CHARME)},
	EDITOR = {Hon F. li and David K. Probst},
	PAGES = {5--22},
	PUBLISHER = {Chapman \& Hall},
	MONTH = oct,
	YEAR = 1997,
	ADDRESS = {Montreal, Canada}
}

@inproceedings{Miner&Johnson96,
	TITLE = {Verification of an Optimized Fault-Tolerant Clock Synchronization
		Circuit: A case study exploring the boundary between
		formal reasoning systems},
	AUTHOR = {Paul S. Miner and Steven D. Johnson},
	BOOKTITLE = {Designing Correct Circuits},
	EDITOR = {Mary Sheeran and Satnam Singh},
	PUBLISHER = {Electronic Workshops in Computing (\url{http://ewic.org.uk/ewic/})},
	MONTH = sep,
	YEAR = 1996,
	ADDRESS = {Bastad, Sweden}
}

@inproceedings{Miner94:circuit,
	TITLE = {Interaction of Formal Design Systems in the Development
		of a Fault-Tolerant Clock Synchronization Circuit},
	AUTHOR = {Paul S. Miner and Shyamsundar Pullela and Steven D.
		Johnson},
	BOOKTITLE = {13th Symposium on Reliable Distributed Systems},
	PAGES = {128--137},
	MONTH = oct,
	YEAR = 1994,
	ORGANIZATION = {IEEE Computer Society},
	ADDRESS = {Dana Point, CA}
}

@inproceedings{Miner96:FMCAD,
	TITLE = {Verification of {IEEE} Compliant Subtractive Division
		Algorithms},
	AUTHOR = {Paul S. Miner and James F. {Leathrum, Jr.}},
	BOOKTITLE = {Formal Methods in Computer-Aided Design (FMCAD '96)},
	EDITOR = {Mandayam Srivas and Albert Camilleri},
	PAGES = {64--78},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1166,
	MONTH = nov,
	YEAR = 1996,
	ADDRESS = {Palo Alto, CA}
}

@inproceedings{Miller&Srivas95,
	TITLE = {Formal Verification of the {AAMP5} Microprocessor: A
		Case Study in the Industrial Use of Formal Methods},
	AUTHOR = {Steven P. Miller and Mandayam Srivas},
	BOOKTITLE = {WIFT '95: Workshop on Industrial-Strength Formal
		Specification Techniques},
	PAGES = {2--16},
	YEAR = 1995,
	ORGANIZATION = {IEEE Computer Society},
	ADDRESS = {Boca Raton, FL}
}

@inproceedings{Pnueli98:FMCAD,
	TITLE = {Verification of Data-Insensitive Circuits: An In-Order-Retirement
		Case Study},
	AUTHOR = {Amir Pnueli and Tamara Arons},
	BOOKTITLE = {Formal Methods in Computer-Aided Design (FMCAD '98)},
	EDITOR = {Ganesh Gopalakrishnan and Phillip Windley},
	PAGES = {351--368},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1522,
	MONTH = nov,
	YEAR = 1998,
	ADDRESS = {Palo Alto, CA}
}

@inproceedings{Ruess96:CAV,
	TITLE = {Modular Verification of {SRT} Division},
	AUTHOR = {H. Rue{\ss} and N. Shankar and M. K. Srivas},
	BOOKTITLE = {Computer-Aided Verification, CAV '96},
	EDITOR = {Rajeev Alur and Thomas A. Henzinger},
	PAGES = {123--134},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1102,
	MONTH = {July/August},
	YEAR = 1996,
	ADDRESS = {New Brunswick, NJ}
}

@article{Ruess99:FMSD,
	TITLE = {Modular Verification of {SRT} Division},
	AUTHOR = {H. Rue{\ss} and N. Shankar and M. K. Srivas},
	JOURNAL = {Formal Methods in Systems Design},
	PAGES = {45--73},
	VOLUME = 14,
	NUMBER = 1,
	MONTH = jan,
	YEAR = 1999
}

@inproceedings{Sree97:AMAST,
	TITLE = {{ATM} Switch Design: Parametric High-Level Modeling
		and Formal Verification},
	AUTHOR = {Sreeranga P. Rajan and Masahiro Fujita},
	BOOKTITLE = {Algebraic Methodology and Software Technology, {AMAST}'97},
	EDITOR = {Michael Johnson},
	PAGES = {437--450},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1349,
	MONTH = dec,
	YEAR = 1997,
	ADDRESS = {Sydney, Australia}
}

@article{Sree98:todaes,
	TITLE = {{ATM} Switch Design by High Level Modeling, Formal Verification,
		and High Level Synthesis},
	AUTHOR = {S. P. Rajan and M. Fujita and K. Yuan and M. T-C. Lee},
	JOURNAL = {ACM Transactions on Design Automation of Electronic
		Systems (TODAES)},
	PAGES = {554--562},
	VOLUME = 3,
	NUMBER = 4,
	MONTH = oct,
	YEAR = 1998
}

@inproceedings{Srivas&Miller95:chdl,
	TITLE = {Applying Formal Verification to a Commercial Microprocessor},
	AUTHOR = {Mandayam K. Srivas and Steven P. Miller},
	BOOKTITLE = {{CHDL '95}: 12th Conference on Computer Hardware
		Description Languages and their Applications},
	EDITOR = {Steven D. Johnson},
	PAGES = {493--502},
	MONTH = aug,
	YEAR = 1995,
	ORGANIZATION = {Proceedings published in a single volume jointly
		with ASP-DAC '95, CHDL '95, and VLSI '95, IEEE Catalog
		no.\ 95TH8102},
	ADDRESS = {Chiba, Japan}
}

@incollection{Srivas&Miller95:inbook,
	TITLE = {Formal Verification of the {AAMP5} Microprocessor},
	AUTHOR = {Mandayam K. Srivas and Steven P. Miller},
	BOOKTITLE = {Applications of Formal Methods},
	CHAPTER = 7,
	EDITOR = {Michael G. Hinchey and Jonathan P. Bowen},
	PAGES = {125--180},
	PUBLISHER = {Prentice Hall},
	SERIES = {Prentice Hall International Series in Computer Science},
	YEAR = 1995,
	ADDRESS = {Hemel Hempstead, UK}
}

@article{Srivas&Miller96:FMSD,
	TITLE = {Applying Formal Verification to the {AAMP5} Microprocessor:
		A Case Study in the Industrial Use of Formal Methods},
	AUTHOR = {Mandayam K. Srivas and Steven P. Miller},
	JOURNAL = {Formal Methods in Systems Design},
	PAGES = {153--188},
	VOLUME = 8,
	NUMBER = 2,
	MONTH = mar,
	YEAR = 1996
}

@article{Mansouri00:FMSD,
	TITLE = {Automated Correctness Condition Generation for Formal
		Verification of Synthesized {RTL} Designs},
	AUTHOR = {Nazanin Mansouri and Ranga Vemuri},
	JOURNAL = {Formal Methods in Systems Design},
	PAGES = {59--91},
	VOLUME = 16,
	NUMBER = 1,
	MONTH = jan,
	YEAR = 2000
}

@inproceedings{Naren98:ICCD,
	TITLE = {Theorem Proving Guided Development of Formal Assertions
		in a Resource-Constrained Scheduler for High-Level Synthesis},
	AUTHOR = {Naren Narasimhan and Elena Teica and Rajesh Radhakrishnan
		and Sriram Govindarajan and Ranga Vemuri},
	BOOKTITLE = {International Conference on Computer Design ({ICCD}'98)},
	EDITOR = {Andreas Kuehlmann},
	MONTH = oct,
	YEAR = 1998,
	ORGANIZATION = {IEEE Computer Society},
	ADDRESS = {Austin, TX}
}

@inproceedings{Naren98:tphols,
	TITLE = {On the Effectiveness of Theorem Proving Guided Discovery
		of Formal Assertions for a Register Allocator in a High-Level
		Synthesis System},
	AUTHOR = {Naren Narasimhan and Ranga Vemuri},
	BOOKTITLE = {Theorem Proving in Higher Order Logics: 11th International
		Conference, {TPHOLs '98}},
	EDITOR = {Jim Grundy and Malcolm Newey},
	PAGES = {367--386},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1479,
	MONTH = sep,
	YEAR = 1998,
	ADDRESS = {Canberra, Australia}
}

@techreport{Sree94:Philips,
	TITLE = {Transformations in High Level Synthesis: Specification
		and Verification},
	AUTHOR = {P. Sreeranga Rajan},
	NUMBER = {NL-TN 118/94},
	MONTH = apr,
	YEAR = 1994,
	INSTITUTION = {Philips Research Laboratories},
	ADDRESS = {Eindhoven, The Netherlands},
	NOTE = {Revised version available as SRI Technical Report SRI-CSL-94-10,
		October 1994}
}

@inproceedings{Sree95:chdl,
	TITLE = {Correctness of Transformations in High Level Synthesis},
	AUTHOR = {Sreeranga P. Rajan},
	BOOKTITLE = {{CHDL '95}: 12th Conference on Computer Hardware
		Description Languages and their Applications},
	EDITOR = {Steven D. Johnson},
	PAGES = {597--603},
	MONTH = aug,
	YEAR = 1995,
	ORGANIZATION = {Proceedings published in a single volume jointly
		with ASP-DAC '95, CHDL '95, and VLSI '95, IEEE Catalog
		no.\ 95TH8102},
	ADDRESS = {Chiba, Japan}
}

@phdthesis{Sree:thesis,
	TITLE = {Transformations on Dependency Graphs: Formal Specification
		and Efficient Mechanical Verification},
	AUTHOR = {Sreeranga P. Rajan},
	MONTH = oct,
	YEAR = 1995,
	SCHOOL = {Department of Computer Science, University of British
		Columbia},
	ADDRESS = {Vancouver, Canada}
}

@inproceedings{Nalumasu&Ganesh98,
	TITLE = {Deriving Efficient Cache Coherence Protocols Through
		Refinement},
	AUTHOR = {Ratan Nalumasu and Ganesh Gopalakrishnan},
	BOOKTITLE = {Formal Methods for Parallel Programming: Theory
		and Applications {(FMPPTA)}},
	MONTH = mar,
	YEAR = 98,
	ADDRESS = {Orlando, FL},
	NOTE = {Available at \url{http://www.loria.fr/~mery/lncs_fmppta98/paper7.ps}}
}

@phdthesis{Park:thesis,
	TITLE = {Computer Assisted Analysis of Multiprocessor Memory
		Systems},
	AUTHOR = {Seungjoon Park},
	MONTH = jun,
	YEAR = 1996,
	SCHOOL = {Department of Electrical Engineering, Stanford University}
}

@unpublished{Park&Dill96:PDS,
	TITLE = {An Executable Specification, Analyzer and Verifier for
		Relaxed Memory Order: With Formal Proofs},
	AUTHOR = {Seungjoon Park and David L. Dill},
	YEAR = 1996,
	NOTE = {Submitted for publication; an earlier version (without
		proofs) is available~\cite{Park&Dill95:spaa}}
}

@article{Park&Dill98:TCS,
	TITLE = {Verification of Cache Coherence Protocols by Aggregation
		of Distributed Transactions},
	AUTHOR = {Seungjoon Park and David L. Dill},
	JOURNAL = {Theory of Computing Systems},
	PAGES = {355--376},
	VOLUME = 31,
	NUMBER = 4,
	YEAR = 1998
}

@inproceedings{Rajan95:multimedia,
	TITLE = {A Formal Basis for Structured Multimedia Collaborations},
	AUTHOR = {Sreeranga Rajan and P. Venkat Rangan and Harrick M.
		Vin},
	BOOKTITLE = {Proceedings of the 2nd IEEE International Conference
		on Multimedia Computing and Systems},
	PAGES = {194--201},
	MONTH = may,
	YEAR = 1995,
	ORGANIZATION = {IEEE Computer Society},
	ADDRESS = {Washington, DC}
}

@inproceedings{rbj00,
	TITLE = {An Approach to Symbolic Test Generation},
	AUTHOR = {V. Rusu and L. du Bousquet and T. J\'{e}ron},
	BOOKTITLE = {2nd International Workshop on Integrated Formal
		Method (IFM'00)},
	PAGES = {338-357},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	NUMBER = 1945,
	MONTH = nov,
	YEAR = 2000,
	ADDRESS = {Dagstuhl, Germany}
}

@inproceedings{Graham96,
	TITLE = {A Method for the Formal Testing of Program Visualization
		Tools},
	AUTHOR = {T. C. Nicholas Graham},
	BOOKTITLE = {Proceedings of the Fourth Workshop on Program Comprehension},
	PAGES = {45--54},
	PUBLISHER = {IEEE Computer Society},
	MONTH = mar,
	YEAR = 1996,
	ADDRESS = {Berlin, Germany}
}

@inproceedings{Suri&Sinha98,
	TITLE = {On the Use of Formal Methods for Validation},
	AUTHOR = {Neeraj Suri and Purnendu Sinha},
	BOOKTITLE = {Fault Tolerant Computing Symposium 28},
	PAGES = {390--399},
	MONTH = jun,
	YEAR = 1998,
	ORGANIZATION = {IEEE Computer Society},
	ADDRESS = {Munich, Germany}
}

@inproceedings{Sinha&Suri99:FTCS,
	TITLE = {Identification of Test Cases Using a Formal Fault Injection
		Approach},
	AUTHOR = {Purnendu Sinha and Neeraj Suri},
	BOOKTITLE = {Fault Tolerant Computing Symposium 29},
	PAGES = {314--321},
	MONTH = jun,
	YEAR = 1999,
	ORGANIZATION = {IEEE Computer Society},
	ADDRESS = {Madison, WI}
}

@inproceedings{Sinha&Suri99:RTSS,
	TITLE = {Formal Techniques for Dependable Real Time Protocols},
	AUTHOR = {Purnendu Sinha and Neeraj Suri},
	BOOKTITLE = {Real Time Systems Symposium},
	MONTH = dec,
	YEAR = 1999,
	ORGANIZATION = {IEEE Computer Society},
	ADDRESS = {Phoenix, AZ}
}

@inproceedings{Qadeer&Shankar98,
	TITLE = {Verifying a Self-Stabilizing Mutual Exclusion Algorithm},
	AUTHOR = {Shaz Qadeer and Natarajan Shankar},
	BOOKTITLE = {IFIP International Conference on Programming Concepts
		and Methods (PROCOMET '98)},
	EDITOR = {David Gries and Willem-Paul de Roever},
	PAGES = {424--443},
	PUBLISHER = {Chapman \& Hall},
	MONTH = jun,
	YEAR = 1998,
	ADDRESS = {Shelter Island, NY}
}

@inproceedings{Kulkarni99:SSS,
	TITLE = {A Case Study in Component-based Mechanical Verification
		of Fault-Tolerant Programs},
	AUTHOR = {Sandeep Kulkarni and John Rushby and N. Shankar},
	BOOKTITLE = {{ICDCS} Workshop on Self-Stabilizing Systems},
	PAGES = {33--40},
	MONTH = jun,
	YEAR = 1999,
	ORGANIZATION = {IEEE Computer Society},
	ADDRESS = {Austin, TX}
}

@inproceedings{Gargantini&Riccobene00:ASM,
	TITLE = {Encoding {Abstract State Machines} in {PVS}},
	AUTHOR = {Angelo Gargantini and Elvinia Riccobene},
	BOOKTITLE = {Abstract State Machines: Theory and Applications
		({ASM} 2000)},
	EDITOR = {Yuri Gurevich and Phillip W. Kutter and Martin Odersky
		and Lothar Thiele},
	PAGES = {303--322},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	NUMBER = 1912,
	MONTH = mar,
	YEAR = 2000,
	ADDRESS = {Monte Verit\`{a}, Switzerland}
}

@inproceedings{Bodeveix-etal99,
	TITLE = {A Formalization of the {B-Method} in {Coq} and {PVS}},
	AUTHOR = {Jean Paul Bodeveix and Mamoun Filali and C\'{e}sar
		A. Mu{\~{n}}oz},
	BOOKTITLE = {FM99: The World Congress in Formal Methods, User
		Group Meeting 2. The B-Method: Applying B in an Industrial
		Context: Tools, Lessons and Techniques},
	MONTH = sep,
	YEAR = 1999,
	NOTE = {Available on the CD-ROM for \cite{FM99}}
}

@inproceedings{Munoz&Rushby:FM99,
	TITLE = {Structural Embeddings: Mechanization with Method},
	AUTHOR = {C\'{e}sar Mu{\~{n}}oz and John Rushby},
	BOOKTITLE = {FM99: The World Congress in Formal Methods},
	EDITOR = {Jeannette Wing and Jim Woodcock},
	PAGES = {452--471},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = {1708 and 1709},
	MONTH = sep,
	YEAR = 1999,
	ADDRESS = {Toulouse, France},
	NOTE = {Pages 1--938 are in the first volume, 939--1872 in the
		second.}
}

@inproceedings{Paige&Ostroff:FM99,
	TITLE = {Developing {BON} as an Industrial-Strength Formal Method},
	AUTHOR = {Richard F. Paige and Jonathan S. Ostroff},
	BOOKTITLE = {FM99: The World Congress in Formal Methods},
	EDITOR = {Jeannette Wing and Jim Woodcock},
	PAGES = {834--853},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = {1708 and 1709},
	MONTH = sep,
	YEAR = 1999,
	ADDRESS = {Toulouse, France},
	NOTE = {Pages 1--938 are in the first volume, 939--1872 in the
		second.}
}

@inproceedings{Bensalem99:DCCA,
	TITLE = {A Methodology for Proving Control Systems with {Lustre}
		and {PVS}},
	AUTHOR = {S. Bensalem and P. Caspi and C. Parent-Vigouroux and
		C. Dumas},
	BOOKTITLE = {Dependable Computing for Critical Applications---7},
	EDITOR = {Charles B. Weinstock and John Rushby},
	PAGES = {89--107},
	PUBLISHER = {IEEE Computer Society},
	SERIES = {Dependable Computing and Fault Tolerant Systems},
	VOLUME = 12,
	MONTH = jan,
	YEAR = 1999,
	ADDRESS = {San Jose, CA}
}

@inproceedings{Rushby&Srivas:HOL93,
	TITLE = {Using {PVS} to Prove Some Theorems of {David Parnas}},
	AUTHOR = {John Rushby and Mandayam Srivas},
	BOOKTITLE = {Higher Order Logic Theorem Proving and its Applications
		(6th International Workshop, HUG '93)},
	EDITOR = {Jeffrey J. Joyce and Carl-Johan H. Seger},
	PAGES = {163--173},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 780,
	MONTH = aug,
	YEAR = 1993,
	ADDRESS = {Vancouver, Canada}
}

@inproceedings{Heimdahl&Czerny96,
	TITLE = {Using {PVS} to Analyze Hierarchical State-Based Requirements
		for Completeness and Consistency},
	AUTHOR = {Mats P. E. Heimdahl and Barbara J. Czerny},
	BOOKTITLE = {IEEE High-Assurance Systems Engineering Workshop
		(HASE '96)},
	PAGES = {252--262},
	MONTH = oct,
	YEAR = 1996,
	ADDRESS = {Niagara on the Lake, Canada}
}

@inproceedings{Heimdahl97:LFM,
	TITLE = {Verifying Communication Related Safety Constraints in
		{RSML} Specifications},
	AUTHOR = {Mats P.E. Heimdahl},
	BOOKTITLE = {LFM' 97: Fourth NASA Langley Formal Methods Workshop},
	EDITOR = {C. Michael Holloway and Kelly J. Hayhurst},
	PAGES = {115--128},
	SERIES = {NASA Conference Publication 3356},
	MONTH = sep,
	YEAR = 1997,
	ORGANIZATION = {NASA Langley Research Center},
	ADDRESS = {Hampton, VA},
	NOTE = {Available at \url{http://atb-www.larc.nasa.gov/Lfm97/proceedings/}}
}

@inproceedings{Heimdahl97:ICFEM,
	TITLE = {Specification and Analysis of System Level Inter-Component
		Communication},
	AUTHOR = {Mats P. E. Heimdahl and Jeffrey M. Thompson},
	BOOKTITLE = {First International Conference on Formal Engineering
		Methods (ICFEM '97)},
	EDITOR = {Michael G. Hinchey and Shaoying Liu},
	PAGES = {192--201},
	MONTH = nov,
	YEAR = 1997,
	ORGANIZATION = {IEEE Computer Society},
	ADDRESS = {Hiroshima, Japan}
}

@inproceedings{Czerny&Heimdahl:ASE98,
	TITLE = {Automated Integrative Analysis of State-based Requirements},
	AUTHOR = {Barbara J. Czerny and Mats P. E. Heimdahl},
	BOOKTITLE = {Thirteenth IEEE Conference on Automated Software
		Engineering ({ASE '98})},
	EDITOR = {D. Redmiles and B. Nuseibeh},
	MONTH = oct,
	YEAR = 1998,
	ORGANIZATION = {IEEE Computer Society},
	ADDRESS = {Nonolulu, Hawaii}
}

@article{Heimdahl98:computer,
	TITLE = {Specification and Analysis of Intercomponent Communication},
	AUTHOR = {Mats P. E. Heimdahl and Jeffrey M. Thompson and Barbara
		J. Czerny},
	JOURNAL = {IEEE Computer},
	PAGES = {47--54},
	VOLUME = 31,
	NUMBER = 4,
	MONTH = apr,
	YEAR = 1998
}

@inproceedings{Agerholm96,
	TITLE = {Translating Specifications in {VDM-SL} to {PVS}},
	AUTHOR = {Sten Agerholm},
	BOOKTITLE = {Theorem Proving in Higher Order Logics: 9th International
		Conference, {TPHOLs '96}},
	EDITOR = {Joakim von Wright and Jim Grundy and John Harrison},
	PAGES = {1--16},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1125,
	MONTH = aug,
	YEAR = 1996,
	ADDRESS = {Turku, Finland}
}

@incollection{Agerholm97:VDMbook,
	TITLE = {On the Verification of {VDM} Specification and Refinement
		with {PVS}},
	AUTHOR = {Sten Agerholm and Juan Bicarregui and Savi Maharaj},
	BOOKTITLE = {Proof in {VDM}: Case Studies},
	CHAPTER = 6,
	EDITOR = {Juan Bicarregui},
	PAGES = {157--190},
	PUBLISHER = {Springer-Verlag},
	SERIES = {FACIT (Formal Approaches to Computing and Information
		Technology)},
	YEAR = 1997,
	ADDRESS = {London, UK}
}

@inproceedings{Maharaj97:ASE,
	TITLE = {On the Verification of {VDM} Specification and Refinement
		with {PVS}},
	AUTHOR = {Savi Maharaj and Juan Bicarregui},
	BOOKTITLE = {12th IEEE International Conference on Automated
		Software Engineering ({ASE '97})},
	EDITOR = {M. Lowry and Y. Ledru},
	PAGES = {280--289},
	MONTH = nov,
	YEAR = 1997,
	ORGANIZATION = {IEEE Computer Society},
	ADDRESS = {Incline Village, NV}
}

@inproceedings{Alexander-etal:FM99,
	TITLE = {A Brief Summary of {VSPEC}},
	AUTHOR = {Perry Alexander and Murali Rangarajan and Phillip Baraona},
	BOOKTITLE = {FM99: The World Congress in Formal Methods},
	EDITOR = {Jeannette Wing and Jim Woodcock},
	PAGES = {1068--1086},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = {1708 and 1709},
	MONTH = sep,
	YEAR = 1999,
	ADDRESS = {Toulouse, France},
	NOTE = {Pages 1--938 are in the first volume, 939--1872 in the
		second.}
}

@inproceedings{Adams-etal:CADE99,
	TITLE = {{VSDITLU}: A Verifiable Symbolic Definite Integral Table
		Look-Up},
	AUTHOR = {A. A. Adams and H. Gottliebsen and S. A. Linton and
		U. Martin},
	BOOKTITLE = {Automated Deduction---{CADE-16}},
	PAGES = {112--126},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Artificial Intelligence},
	VOLUME = 1632,
	MONTH = jul,
	YEAR = 1999,
	ADDRESS = {Trento, Italy}
}

@inproceedings{Adams-etal:ISSAC99,
	TITLE = {Automated Theorem Proving in Support of Computer Algebra:
		Symbolic Definite Integration as a Case Study},
	AUTHOR = {A. A. Adams and H. Gottliebsen and S. A. Linton and
		U. Martin},
	BOOKTITLE = {Proceedings of the 1999 International Symposium
		on Symbolic and Algebraic Computation, ({ISSAC '99})},
	PAGES = {253--260},
	MONTH = jul,
	YEAR = 1999,
	ORGANIZATION = {Association for Computing Machinery},
	ADDRESS = {Vancouver, B.C., Canada}
}

@inproceedings{Buth98:TOOLS96,
	TITLE = {Combining Tools for the Verification of Fault-Tolerant
		Systems},
	AUTHOR = {Bettina Buth and Rachel Cardell-Oliver and Jan Peleska},
	BOOKTITLE = {Tools for System Development and Verification},
	EDITOR = {Bettina Buth and Rudolf Berghammer and Jan Peleska},
	PAGES = {41--69},
	PUBLISHER = {Shaker Verlag},
	SERIES = {BISS Monographs},
	YEAR = 1998,
	ADDRESS = {Aachen, Germany},
	NOTE = {Proceedings of a workshop held at Bremen in 1996}
}

@inproceedings{Buth98:tools,
	TITLE = {{PAMELA} + {PVS}},
	AUTHOR = {Bettina Buth},
	BOOKTITLE = {Tool Support for System Specification, Development,
		and Verification},
	EDITOR = {Rudolph Berghammer and Yassine Lakhnech},
	PAGES = {62--76},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Advances in Computing Science},
	MONTH = jun,
	YEAR = 1998,
	ADDRESS = {Malente, Germany},
	NOTE = {Proceedings published in May 1999}
}

@inproceedings{Buth97:AMAST,
	TITLE = {{PAMELA $+$ PVS}},
	AUTHOR = {Bettina Buth},
	BOOKTITLE = {Algebraic Methodology and Software Technology, {AMAST}'97},
	EDITOR = {Michael Johnson},
	PAGES = {560--562},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1349,
	MONTH = dec,
	YEAR = 1997,
	ADDRESS = {Sydney, Australia}
}

@inproceedings{Corbett-etal00:ICSE,
	TITLE = {Bandera: Extracting Finite-state Models from {Java}
		Source Code},
	AUTHOR = {James Corbett and Matthew Dwyer and John Hatcliff and
		Corina Pasareanu and Robby and Shawn Laubach and Hongjun
		Zheng},
	BOOKTITLE = {22nd International Conference on Software Engineering},
	PAGES = {439--448},
	MONTH = jun,
	YEAR = 2000,
	ORGANIZATION = {IEEE Computer Society},
	ADDRESS = {Limerick, Ireland}
}

@proceedings{Compass89,
	TITLE = {COMPASS '89 (Proceedings of the Fourth Annual Conference
		on Computer Assurance)},
	BOOKTITLE = {COMPASS '89 (Proceedings of the Fourth Annual Conference
		on Computer Assurance)},
	MONTH = jun,
	YEAR = 1989,
	ORGANIZATION = {IEEE Washington Section},
	ADDRESS = {Gaithersburg, MD}
}

@proceedings{FTCS-highlights,
	TITLE = {Fault Tolerant Computing Symposium 25: Highlights from
		25 Years},
	BOOKTITLE = {Fault Tolerant Computing Symposium 25: Highlights
		from 25 Years},
	PUBLISHER = {IEEE Computer Society},
	MONTH = jun,
	YEAR = 1995,
	ORGANIZATION = {IEEE Computer Society},
	ADDRESS = {Pasadena, CA}
}

@article{Saiedian96,
	TITLE = {An Invitation to Formal Methods},
	AUTHOR = {Hossein {Saiedian (Ed.)}},
	JOURNAL = {IEEE Computer},
	PAGES = {16--30},
	VOLUME = 29,
	NUMBER = 4,
	MONTH = apr,
	YEAR = 1996,
	NOTE = {A ``roundtable'' of short articles by several authors.}
}

@proceedings{Encress95,
	TITLE = {Safety and Reliability of Software Based Systems (Twelfth
		Annual {CSR} Workshop)},
	BOOKTITLE = {Safety and Reliability of Software Based Systems
		(Twelfth Annual {CSR} Workshop)},
	EDITOR = {Roger Shaw},
	PUBLISHER = {Springer},
	MONTH = sep,
	YEAR = 1995,
	ADDRESS = {Bruges, Belgium}
}

@inproceedings{Park&Dill95:spaa,
	TITLE = {An Executable Specification, Analyzer and Verifier for
		{RMO (Relaxed Memory Order)}},
	AUTHOR = {Seungjoon Park and David L. Dill},
	BOOKTITLE = {7th ACM Symposium on Parallel Algorithms and Architectures},
	PAGES = {34--51},
	MONTH = jul,
	YEAR = 1995
}

@proceedings{FM99,
	TITLE = {FM99: The World Congress in Formal Methods},
	BOOKTITLE = {FM99: The World Congress in Formal Methods},
	EDITOR = {Jeannette Wing and Jim Woodcock},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = {1708 and 1709},
	MONTH = sep,
	YEAR = 1999,
	ADDRESS = {Toulouse, France},
	NOTE = {Pages 1--938 are in the first volume, 939--1872 in the
		second.}
}