\documentstyle[11pt,cite,url]{article}
\sloppy
\topmargin -0.25in
\textwidth 5.75in
\textheight 8.25in
\oddsidemargin .53in
\evensidemargin .28in
\def\BibTeX{{\rm B\kern-.05em{\sc i\kern-.025em b}\kern-.08em
    T\kern-.1667em\lower.7ex\hbox{E}\kern-.125emX}}
\title{\bf PVS Bibliography}
\author{John Rushby\\
Computer Science Laboratory\\
SRI International\\
Menlo Park CA 94025 USA
\\ \mbox{ }\\
Email: {\tt pvs-request@csl.sri.com}
\\WWW: \url{http://www.csl.sri.com/pvs.html}
}
\begin{document}
\maketitle

This bibliography lists most of the publications that I am aware of
concerning the development and application of the PVS verification
system and its predecessors.  The files used to create this report, including
the \BibTeX\ bibliography, are available at
\url{http://www.csl.sri.com/pvs-bib.html}.  PVS users are
encouraged to use the \BibTeX\ entries from these files, which are as
accurate, complete, and up to date as I can make them.  

I have limited this list to publications that should be available in
a university or research library.  For this reason, I have omitted
citations to conference proceedings that were not issued by a
technical society or commercial publisher, unless they are on the
Web; similarly, technical reports are cited only when they are widely
distributed (e.g., NASA), or where there is no other source and they
are are on the Web (or otherwise freely available, if they predate
the Web).  Many of the journal and conference papers listed are
supported by technical reports that provide much more detail; I am
willing to add these if there is demand.  Because papers are often
available on the web in advance of the journal or proceedings in which
they will appear, I now include such papers and mark them ``to appear.''

Most of the publications later than about 1990, and some earlier
ones, are available on the Web from
\url{http://www.csl.sri.com/fm-papers.html} (for SRI papers) or
\url{http://www.csl.sri.com/pvs-users.html} (for others); hard copies
of all these papers are available at SRI.
Many papers are archived at the NECI Scientific Literature Digital Library
\url{http://citeseer.nj.nec.com/cs} and at
The Hypatia Digital Library at \url{http://hypatia.dcs.qmw.ac.uk/} or
can be found on the authors' home pages, which can usually be tracked
down using a search engine such as \url{www.google.com}.

Please keep me informed of new papers (or forgotten historical ones)
that should be added to this collection, and of any inaccuracies.

\subsection*{History}

PVS is the most recent in a line of specification languages, theorem
provers, and verification systems developed at SRI that goes back over
20 years.  Early systems included the Jovial Verification
System~\cite{jovial:pv} (Jovial was a language based on Algol 58, a
precursor to the more famous Algol 60, that was used by the US Air
Force), and the Hierarchical Development Methodology
(HDM)~\cite{Robinson&Levitt,
HDM:Handbook,
Spitzen:example}.
HDM had a ``security analyzer''~\cite{Feiertag:Tool}
based on information flow~\cite{FLR77} that was used in the
verification of the Honeywell SCOMP~\cite{Benzel:scomp-eval,
Silverman83} (the first computer to gain the
NSA's A1~\cite{Criteria} rating) and several other
secure systems~\cite{Lindsay88:Regency,
Regency88}.

The HDM security flow analyzer used the Boyer-Moore theorem prover, much of
whose early development was performed at SRI~\cite{Boyer-Moore79}.
A parallel development was Shostak's Theorem Prover STP~\cite{STP},
which was based on his decision procedures~\cite{Shostak:sup-inf,
Shostak:equality,
Shostak:arithmetic,
Shostak:residues,
Shostak:combination} and used in the analysis of some aspects of the
SIFT flight control computer~\cite{Weinstock80,
SIFT-design}\footnote{Although the SIFT verification was a
significant accomplishment at the time, the paper describing
it~\cite{Sift-verif} leaves the impression that the full operating
system was verified, as opposed to some properties of its design.
This led to severe criticism by a NASA peer
review~\cite{SIFT:review}.} and early experiments in hardware
verification~\cite{Shostak:circuits}.

HDM and STP were the main design influences on ``Enhanced HDM'' ({\sc
Ehdm}), whose development began in 1983.  
{\sc Ehdm} introduced the higher-order specification language with
theory-level (they are called ``modules'' in {\sc Ehdm})
parameterization that provides much of the foundation for the PVS language.
{\sc Ehdm} was operational
by 1985~\cite{Kemmerer:assess,
Melliar-Smith&Rushby,
Rushby:HDM} and was further developed through the following
decade~\cite{EHDM:Overview88,
EHDM:tutorial}.\footnote{{\sc Ehdm}
has some capabilities currently lacking in PVS: for example,
hierarchical development based on theory interpretations, imperative
program verification using a small subset of a Pascal-like language,
a superior prover interface (to an interactive prover derived from
that of PVS) and more capable (though slower) arithmetic decision
procedures.  However, it lacks some of the linguistic capabilities of
PVS: for example, dependent typing, abstract data types, inductive
relations, and several type constructors.
{\sc Ehdm} continues to be available,
but its distribution is controlled by the US Government.}
Verification of fault-tolerant algorithms
and architectures provided the biggest applications of {\sc
Ehdm}~\cite{DiVito-DCCA-3,
Miner93,
Rushby92:OM,
Rushby93:masking,
Rushby94:icah,
Rushby&vonHenke93,
Shankar:clocks:Nijmegen}, and some small experiments in hardware
verification~\cite{Butler-Sjogren91,
Joyce&all:compcon}
were also performed.

PVS was started in late 1990 as an SRI-funded research program to
prototype ideas for an interactive prover for {\sc Ehdm} and the
design of a ``next generation'' verification system (hence its
original name---``{\em Prototype\/} Verification System'').  SRI made
the first version of PVS freely available in 1993~\cite{PVS:tutorial}
and it proved so popular that we have continued to develop it ever
since (first with SRI IR\&D funds, and later with additional support
from NASA, NRL, AFOSR, ARPA, and NSF).

\subsection*{Documentation and Availability}

PVS is freely available under license from SRI\@.  Information,
examples, papers, documentation, and the system itself are available
from the PVS home page at \url{http://www.csl.sri.com/pvs.html} and
the CSL ftp server at \url{ftp://ftp.csl.sri.com/pub/pvs}, and from
mirror sites in England, France, Germany, and Japan.\footnote{These
sites are \url{ftp://ftp.cs.york.ac.uk/pub/pvs} at the University of
York, England; \url{ftp://ftp.ibp.fr/pub/pvs} at the University of
Paris VI, France; \url{ftp://ftp.informatik.uni-ulm.de/pub/KI/pvs} at
the University of Ulm, Germany; and
\url{ftp://nicosia.is.s.u-tokyo.ac.jp/pub/misc/pvs} at Tokyo
University, Japan.}

The PVS system is described briefly in three system
descriptions~\cite{PVS96:CAV,PVS-CADE92,Shankar96:FMCAD}
and an experience report \cite{Owre-etal98:FM-TRENDS}
and fully documented in
separate manuals for the language~\cite{PVS:language},
prover~\cite{PVS:prover},
system~\cite{PVS:userguide},
and
semantics~\cite{PVS-Semantics:TR}.  
Some of the motivation and design decisions for PVS are described
in~\cite{Owre95:prolegomena}, and the utility of its type system is
argued in~\cite{Rushby98:TSE,Shankar&Owre:WADT99}.
Tutorials provide general introductions to PVS~\cite{Butler:PVS-tut,
WIFT-Tut,
Rushby&Stringer-Calvert95},
plus more specialized treatments for hardware~\cite{Owre94:TPCD},
abstract data types~\cite{PVS-ADT:TR},
tabular and requirements
specifications~\cite{Owre95:tables}, and
distributed systems~\cite{FORTE97-Tut,Rushby00:Movep2k}.
General introductions to formal
methods, with PVS examples, are provided by the NASA Guidebook
series~\cite{NASA-GB1,NASA-GB2}.

\subsection*{Methodology and Technology}

Some of the philosophical and methodological ideas behind PVS and its
applications are described in~\cite{Cyrluk&Srivas95:iccd,
Dill&Rushby96,
Rushby92:repsa,
Rushby95:ZUM,
Rushby96:CAV,
Rushby96:FSTTCS,
Rushby97:isre,
Rushby:FM99,
Shankar85,
Shankar:notes,
Shankar:book,
Shankar:FTRTFT96},
while issues in the application of formal methods to safety-critical
systems are described in
\cite{NASA-GB1,
Rushby:FAA-full,
Rushby94:Taxonomy,
Rushby:FAA-short}
and hardware verification is discussed in~\cite{Srivas97:chapter}.

The theorem-proving techniques employed in PVS are described
in~\cite{Cyrluk96:DP,
Cyrluk-etal97:CAV,
Cyrluk94:gtl,
Cyrluk94:TPCD,
Moeller98:FMCAD,
Tiwari-etal00:CADE}, 
and their integration with model checking and with tabular
specifications are described in~\cite{Rajan95:CAV}
and~\cite{pvs-tables:tacas97},
respectively.   Use of a decision procedure for WS1S within PVS is
described in~\cite{Owre&Ruess00:CAV}
Experimental support for efficient evaluation and its
use to support reflection
in PVS are described in~\cite{Pfab98:tools,
vonHenke98:tphols}, while the very efficient evaluator built-in to PVS
2.3 is described in~\cite{shankar99:eval}.
Techniques and tools to support automated generation of abstractions
and invariants in PVS 
are
described in~\cite{Bensalem96:CAV,
Bensalem98:CAV,
Abdulla:CAV99,
Rusu&Singerman99,
Graf96:CAV,
Saidi96,
Saidi97:CAV,
Saidi&Graf97:CAV,
Saidi97:LFM,
Saidi&Shankar:CAV99,
Saidi00:SAS,
Shankar00:ASM,
Shankar00:CONCUR}
and the integration of these capabilities in extensions  to PVS such
as SAL and InVeST are described in
\cite{
Bensalem98:InVeSt,
SALoverview00:LFM,
Rushby98:ICFEM,
Rushby:SPIN99,
Rushby00:Forte,
Rushby00:HASE}.


Comparisons between PVS and ACL2 treatments of an interactive
consistency algorithm~\cite{Young97:IC}, and between PVS and HOL
specifications of the IEEE 854 floating-point
standard~\cite{Miner95:HOL} are available, while Mike Gordon provides a
discussion of PVS from a HOL perspective~\cite{Gordon95:PVS}
and David Griffioen and Marieke Huisman compare PVS and Isabelle/HOL
\cite{Griffioen98:tphols}.  
Jan Friso Groote, Fran\,{c}ois Monin and Jaco van de Pol
provide a tutorial on protocol and distributed systems verification
that considers Isabelle, Coq, and PVS, and makes some
comparison between the systems \cite{Groote-etal98:CONCUR},
while
Kern and Greenstreet survey several methods for hardware
verification, including PVS
\cite{Kern99:todaes}.
Heinrich Rust presents a PVS treatment for an ``invoicing'' example
used in the comparison of many systems~\cite{Rust98}.
Matt Wilding describes an approach, derived from those used with
Nqthm and ACL2, for developing robust proofs of machine code
programs~\cite{Wilding97:LFM}.
Georg Droschl compares some aspects of PVS and VDM on an
industrially-motivated example~\cite{Droschl:IFMW99,
Droschl:FM99}.
Merriam and Harrison provide an examination of interface issues, and
compare PVS with two other systems~\cite{Merriam96}, while
Archer and Heitmeyer describe using PVS to produce ``human-style''
proofs~\cite{Archer&Heitmeyer97:TPHOLS,Archer98:UITP}.   Issues in introducing
formal methods, including PVS, to students and engineers are discussed
by Knight et al~\cite{Knight97:LFM}.

\subsection*{Applications}

PVS has been applied to classical topics in mathematical
analysis (with applicaiton to computer algebra systems)~\cite{Dutertre96,
Gottliebsen00:TPHOLS},
to the modeling of process calculi~\cite{Basten&Hooman99,
Schamschurko98}
and transition systems~\cite{Griffioen98:CAV,
Pnueli98:FTRTFT},
to the specification of abstract datatypes~\cite{Devillers-etal97,
Hensel&Jacobs97,Hensel98:JLC}, classes in object-oriented
languages~\cite{Hensel-etal98,Huisman-etal99:ECOOP,Jacobs98:OOPSLA,Huisman&Jacobs00:TPHOLS},
and Java programs~\cite{Huisman:PhD,Huisman&Jacobs00:FASE,vandenBerg-etal00:WADT},
to critical algorithms for fault tolerance in
automobile and aircraft control
systems~\cite{Lincoln&Rushby93:CAV,
Lincoln&Rushby93:FTCS,
Lincoln&Rushby94:FTP,
Pfeifer99:DCCA,
Pfeifer00:FORTE,
Rushby99:TSE,
Rushby00:CAV,
Schwier98:FTRTFT,
WalterLincolnSuri97},
to partitioning in these systems~\cite{DiVito:partitioningCR,
diVito99:DCCA,
Wilding99:DCCA}
to software requirements and software design for
aircraft~\cite{Butler96:rqts,
Dutertre&Stavridou97,
Dutertre97:LFM} and for
manned~\cite{
Crow&DiVito98:tosem,
Easterbrook-etal98,
HAC-study,
DiVito96,
DiVito00:STTT,
GPS-study,
Hamilton-etal95,
Hamilton-etal95-2}
and interplanetary~\cite{Ampo&Lutz95,
Lutz&Ampo94,Lutz97:LFM} spacecraft,
to aircraft trajectories~\cite{Carreno&Munoz00:TPHOLS,
Carreno&Munoz00:DASC}
to protection systems for nuclear power plants \cite{Lawford-etal00:AMAST,
Koo-etal99},
to command and control~\cite{vandePol98},
to issues in computer security~\cite{Dean97,
Hoffman98:CAV,
Peri96}, active networks~\cite{Dieckman98},
and
cryptographic protocols~\cite{Dutertre&Schneider97,
Millen:FMSP99,
Monniaux99:CSFW,
Ruess&Millen00:FMCS},
to 
operating systems~\cite{Gopi98:FSTTCS},
distributed algorithms~\cite{Couturier98:CAV,
Chkliaev99,
Chkliaev99:AE,
Chkliaev00:ICFEM,
Couturier98:IFMW,
Devillers00:FMSD,
Glusman&Katz:CAV99,
Havelund:FMPPTA99,
Hooman98:EAS,
Jackson98:tphols,
Mokkedem00:FMSD,
Penix98:fmsp,
Umamageswaran98:JSA},
real-time and scheduling~\cite{Alagar-etal99:RTAS,
Alborghetti97:FSE,
Archer&Heitmeyer96,
AHrtssWIP96,
Bun96:ASCI,
Bun97:ASCI,
deBoer96:ftrtft,
DuBois97:isre,
dutertre99b,
Dutertre&Stavridou00:DASC,
Dutertre00:RTSS,
Fowler&Wellings96,
Fowler97:RTSS,
Hooman94,
Hooman96:RPC,
Hooman97:AMAST,
Hooman97:compos,
Kolano99:ARTS,
Kolano-etal00:FASE,
Muthiayen00,
Shankar93:CAV,
Skakkebaek94:thesis,
Skakkebaek&Shankar94},
reactive~\cite{Kellomaki97},
and hybrid systems~\cite{AHhart97,
Henzinger&Rusu98,
Hooman96:boiler},
to embedded systems \cite{Bloo-etal00:SAC,
deJong00:ECBS,
vandePol-etal99:IFM}, distributed
systems~\cite{deBoer&Hulst96,
Chernyskhovsky:FMPPTA99,
Frey99:HICSS,
Hooman98:TOOLS96,
Kellomaki95,
Kellomaki96:tphols,
Lesens&Saidi97,
Shankar93:lazy,
vanHulst:thesis}
and protocols~\cite{Hooman95,
Havelund&Shankar96,
Khune-etal97,
Mokkedem&Leonard00:TPHOLS,
Rusinowitch-etal00:CAV},
to software architecture \cite{Herbert-etal:FM99},
program development~\cite{Hooman97,
Levy&Trilling:FM99,
Verhoeven&Backhouse:FM99},
software development
steps~\cite{Behnke98:TOOLS96,
Dold95,
Dold:PhD,
Shankar:MPC95,
Shankar:SCP96}
and refinement~\cite{Jacobs97,Jacobs97:AMAST,Jackson00:TPHOLS,Knappmann96},
to compilers~\cite{K-HButh95,
Dold-etal97,
DGVZ98,
Dold-etal98:STTT,
Dold&Vialard99,
Stringer-Calvert97,
Stringer-Calvert98:thesis,
Wahab:UWARWICK:CS-RR-354,
Wahab98},
to hardware
design~\cite{Arons99:VLSI,
Arons&Pnueli00:TACAS,
Cyrluk96:FMCAD,
Cyrluk97:ICFEM,
Damm&Pnueli97,
Fisler94:TPCD,
Gopalakrishnan-etal97,
Greve98:FMCAD,
Hardin98:CAV,
Hosabettu98:CAV,
Hosabettu:CAV99,
Hosabettu:CHARME99,
Hosabettu-etal00:CAV,
Johnson94:TPCD,
Johnson&Miner97,
Leathrum97:LFM,
Li-etal97,
Miner&Johnson96,
Miner94:circuit,
Miner96:FMCAD,
Miller&Srivas95,
Pnueli98:FMCAD,
Ruess96:CAV,
Ruess99:FMSD,
Sree97:AMAST,
Sree98:todaes,
Srivas&Miller95:chdl,
Srivas&Miller95:inbook,
Srivas&Miller96:FMSD}
and
synthesis~\cite{Mansouri00:FMSD,
Naren98:ICCD,
Naren98:tphols,
Sree94:Philips,
Sree95:chdl,
Sree:thesis},
to memory models and cache coherence
protocols~\cite{Nalumasu&Ganesh98,
Park:thesis,
Park&Dill96:PDS,
Park&Dill98:TCS},
to multimedia collaborations~\cite{Rajan95:multimedia},
to test generation~\cite{rbj00}
and to testing program visualization tools~\cite{Graham96},
to validating fault-tolerant real-time systems~\cite{Suri&Sinha98,
Sinha&Suri99:FTCS, 
Sinha&Suri99:RTSS}, 
and to self-stabilization~\cite{Qadeer&Shankar98,
Kulkarni99:SSS}.
PVS has also been used to support other specification
notations including 
Abstract State Machines (ASMs)~\cite{Gargantini&Riccobene00:ASM},
the B Method~\cite{Bodeveix-etal99,
Munoz&Rushby:FM99},
BON \cite{Paige&Ostroff:FM99},
Lustre~\cite{Bensalem99:DCCA},
Tabular methods~\cite{Rushby&Srivas:HOL93,
Heimdahl&Czerny96,
Heimdahl97:LFM,
Heimdahl97:ICFEM,
Czerny&Heimdahl:ASE98,
Heimdahl98:computer},
VDM~\cite{Agerholm96,
Agerholm97:VDMbook,
Maharaj97:ASE},
and VSPEC~\cite{Alexander-etal:FM99}, and in conjunction with
computer algebra systems~\cite{Adams-etal:CADE99,
Adams-etal:ISSAC99},
and in combination with other tools~\cite{Buth98:TOOLS96,
Buth98:tools,
Buth97:AMAST,
Corbett-etal00:ICSE}.


\bibliographystyle{unsrt}
\begin{thebibliography}{100}

\bibitem{jovial:pv}
B.~Elspas, M.~Green, M.~Moriconi, and R.~Shostak.
\newblock A {JOVIAL} verifier.
\newblock Technical report, Computer Science Laboratory, SRI International,
  January 1979.

\bibitem{Robinson&Levitt}
Lawrence Robinson and Karl~N. Levitt.
\newblock Proof techniques for hierarchically structured programs.
\newblock {\em Communications of the ACM}, 20(4):271--283, April 1976.

\bibitem{HDM:Handbook}
L.~Robinson, K.~N. Levitt, and B.~A. Silverberg.
\newblock {\em The {HDM} Handbook}.
\newblock Computer Science Laboratory, SRI International, Menlo Park, CA, June
  1979.
\newblock Three Volumes.

\bibitem{Spitzen:example}
Jay~M. Spitzen, Karl~N. Levitt, and Lawrence Robinson.
\newblock An example of hierarchical design and proof.
\newblock {\em Communications of the ACM}, 21(12):1064--1075, December 1978.

\bibitem{Feiertag:Tool}
R.~J. Feiertag.
\newblock A technique for proving specifications are multilevel secure.
\newblock Technical Report CSL-109, Computer Science Laboratory, SRI
  International, Menlo Park, CA, January 1980.

\bibitem{FLR77}
R.~J. Feiertag, K.~N. Levitt, and L.~Robinson.
\newblock Proving multilevel security of a system design.
\newblock In {\em Sixth ACM Symposium on Operating System Principles}, pages
  57--65, November 1977.

\bibitem{Benzel:scomp-eval}
Terry~Vickers Benzel.
\newblock Analysis of a kernel verification.
\newblock In {\em Proceedings of the Symposium on Security and Privacy}, pages
  125--131, Oakland, CA, April 1984. IEEE Computer Society.

\bibitem{Silverman83}
J.~M. Silverman.
\newblock Reflections on the verification of the security of an operating
  system kernel.
\newblock In {\em Ninth ACM Symposium on Operating System Principles}, pages
  143--154, Bretton Woods, NH, October 1983.
\newblock (ACM Operating Systems Review, Vol.\ 17, No.\ 5).

\bibitem{Criteria}
Department of Defense.
\newblock {\em Department of Defense Trusted Computer System Evaluation
  Criteria}, December 1985.
\newblock DOD 5200.28-STD (supersedes CSC-STD-001-83).

\bibitem{Lindsay88:Regency}
Kenneth~S. Lindsay.
\newblock A taxonomy of the causes of proof failures in applications using the
  {HDM} methodology.
\newblock In {\em Fourth Aerospace Computer Security Applications Conference},
  pages 419--423, Orlando, FL, December 1988. IEEE Computer Society.
\newblock Reprinted in~\cite[pp.~79--83]{Compass89}.

\bibitem{Regency88}
Bill Smith, Cynthia Reese, Kenneth~S. Lindsay, and Brian Crane.
\newblock A description of a formal verification and validation {(FVV)}
  process.
\newblock In {\em Fourth Aerospace Computer Security Applications Conference},
  pages 401--408, Orlando, FL, December 1988. IEEE Computer Society.
\newblock Reprinted in~\cite[pp.~71--78]{Compass89}.

\bibitem{Boyer-Moore79}
R.~S. Boyer and J~S. Moore.
\newblock {\em A Computational Logic}.
\newblock Academic Press, New York, NY, 1979.

\bibitem{STP}
R.~E. Shostak, R.~Schwartz, and P.~M. Melliar-Smith.
\newblock {STP}: A mechanized logic for specification and verification.
\newblock In D.~Loveland, editor, {\em 6th International Conference on
  Automated Deduction (CADE)}, volume 138 of {\em Lecture Notes in Computer
  Science}, New York, NY, 1982. Springer-Verlag.

\bibitem{Shostak:sup-inf}
Robert~E. Shostak.
\newblock On the {SUP-INF} method for proving {Presburger} formulas.
\newblock {\em Journal of the ACM}, 24(4):529--543, October 1977.

\bibitem{Shostak:equality}
Robert~E. Shostak.
\newblock An algorithm for reasoning about equality.
\newblock {\em Communications of the ACM}, 21(7):583--585, July 1978.

\bibitem{Shostak:arithmetic}
Robert~E. Shostak.
\newblock A practical decision procedure for arithmetic with function symbols.
\newblock {\em Journal of the ACM}, 26(2):351--360, April 1979.

\bibitem{Shostak:residues}
Robert~E. Shostak.
\newblock Deciding linear inequalities by computing loop residues.
\newblock {\em Journal of the ACM}, 28(4):769--779, October 1981.

\bibitem{Shostak:combination}
Robert~E. Shostak.
\newblock Deciding combinations of theories.
\newblock {\em Journal of the ACM}, 31(1):1--12, January 1984.

\bibitem{Weinstock80}
Charles~B. Weinstock.
\newblock {SIFT}: System design and implementation.
\newblock In {\em Fault Tolerant Computing Symposium 10}, pages 75--77, Kyoto,
  Japan, October 1980. IEEE Computer Society.
\newblock Reprinted in~\cite[pp.\ 29--30]{FTCS-highlights}.

\bibitem{SIFT-design}
John~H. Wensley, Leslie Lamport, Jack Goldberg, Milton~W. Green, Karl~N.
  Levitt, P.~M. Melliar-Smith, Robert~E. Shostak, and Charles~B. Weinstock.
\newblock {SIFT}: Design and analysis of a fault-tolerant computer for aircraft
  control.
\newblock {\em Proceedings of the IEEE}, 66(10):1240--1255, October 1978.

\bibitem{Sift-verif}
P.~M. Melliar-Smith and R.~L. Schwartz.
\newblock Formal specification and verification of {SIFT}: A fault-tolerant
  flight control system.
\newblock {\em IEEE Transactions on Computers}, C-31(7):616--630, July 1982.

\bibitem{SIFT:review}
NASA Conference Publication 2377.
\newblock {\em Peer Review of a Formal Verification/Design Proof Methodology},
  July 1983.

\bibitem{Shostak:circuits}
Robert~E. Shostak.
\newblock Formal verification of circuit designs.
\newblock In T.~Uehara and M.~Barbacci, editors, {\em Computer Hardware
  Description Languages}, pages 13--29. North-Holland, 1983.

\bibitem{Kemmerer:assess}
Richard~A. Kemmerer.
\newblock Verification assessment study final report.
\newblock Technical Report C3-CR01-86, National Computer Security Center, Ft.\
  Meade, MD, 1986.
\newblock 5 Volumes (Overview, Gypsy, Affirm, FDM, and {\sc Ehdm}). US
  distribution only.

\bibitem{Melliar-Smith&Rushby}
P.~Michael Melliar-Smith and John Rushby.
\newblock The {Enhanced HDM} system for specification and verification.
\newblock In {\em Proc.\ VerkShop III}, pages 41--43, Watsonville, CA, February
  1985.
\newblock Published as ACM Software Engineering Notes, Vol.\ 10, No.\ 4, Aug.\
  85.

\bibitem{Rushby:HDM}
John Rushby.
\newblock The security model of {Enhanced HDM}.
\newblock In {\em Proceedings 7th DoD/NBS Computer Security Initiative
  Conference}, pages 120--136, Gaithersburg, MD, September 1984.

\bibitem{EHDM:Overview88}
F.~W. von Henke, J.~S. Crow, R.~Lee, J.~M. Rushby, and R.~A. Whitehurst.
\newblock The {{\sc Ehdm}} verification environment: An overview.
\newblock In {\em Proceedings 11th National Computer Security Conference},
  pages 147--155, Baltimore, MD, October 1988. NBS/NCSC.

\bibitem{EHDM:tutorial}
John Rushby, Friedrich von Henke, and Sam Owre.
\newblock An introduction to formal specification and verification using {{\sc
  Ehdm}}.
\newblock Technical Report SRI-CSL-91-2, Computer Science Laboratory, SRI
  International, Menlo Park, CA, February 1991.

\bibitem{DiVito-DCCA-3}
Ben~L. {Di Vito} and Ricky~W. Butler.
\newblock Formal techniques for synchronized fault-tolerant systems.
\newblock In C.~E. Landwehr, B.~Randell, and L.~Simoncini, editors, {\em
  Dependable Computing for Critical Applications---3}, volume~8 of {\em
  Dependable Computing and Fault-Tolerant Systems}, pages 163--188.
  Springer-Verlag, Vienna, Austria, September 1992.

\bibitem{Miner93}
Paul~S. Miner.
\newblock Verification of fault-tolerant clock synchronization systems.
\newblock NASA Technical Paper 3349, NASA Langley Research Center, Hampton, VA,
  November 1993.

\bibitem{Rushby92:OM}
John Rushby.
\newblock Formal verification of an {Oral Messages} algorithm for interactive
  consistency.
\newblock Technical Report SRI-CSL-92-1, Computer Science Laboratory, SRI
  International, Menlo Park, CA, July 1992.
\newblock Also available as NASA Contractor Report 189704, October 1992.

\bibitem{Rushby93:masking}
John Rushby.
\newblock A fault-masking and transient-recovery model for digital
  flight-control systems.
\newblock In Jan Vytopil, editor, {\em Formal Techniques in Real-Time and
  Fault-Tolerant Systems}, Kluwer International Series in Engineering and
  Computer Science, chapter~5, pages 109--136. Kluwer, Boston, Dordecht,
  London, 1993.

\bibitem{Rushby94:icah}
John Rushby.
\newblock A formally verified algorithm for clock synchronization under a
  hybrid fault model.
\newblock In {\em Thirteenth ACM Symposium on Principles of Distributed
  Computing}, pages 304--313, Los Angeles, CA, August 1994. Association for
  Computing Machinery.
\newblock Also available as NASA Contractor Report 198289.

\bibitem{Rushby&vonHenke93}
John Rushby and Friedrich von Henke.
\newblock Formal verification of algorithms for critical systems.
\newblock {\em IEEE Transactions on Software Engineering}, 19(1):13--23,
  January 1993.

\bibitem{Shankar:clocks:Nijmegen}
Natarajan Shankar.
\newblock Mechanical verification of a generalized protocol for {Byzantine}
  fault-tolerant clock synchronization.
\newblock In J.~Vytopil, editor, {\em Formal Techniques in Real-Time and
  Fault-Tolerant Systems}, volume 571 of {\em Lecture Notes in Computer
  Science}, pages 217--236, Nijmegen, The Netherlands, January 1992.
  Springer-Verlag.

\bibitem{Butler-Sjogren91}
Ricky~W. Butler and Jon~A. Sjogren.
\newblock Formal design verification of digital circuitry.
\newblock {\em Reliability Engineering and System Safety}, 32:67--93, 1991.

\bibitem{Joyce&all:compcon}
J.~Joyce, E.~Liu, J.~Rushby, N.~Shankar, R.~Suaya, and F.~von Henke.
\newblock From formal verification to silicon compilation.
\newblock In {\em IEEE Compcon}, pages 450--455, San Francisco, CA, February
  1991.

\bibitem{PVS:tutorial}
N.~Shankar, S.~Owre, and J.~M. Rushby.
\newblock {\em PVS Tutorial}.
\newblock Computer Science Laboratory, SRI International, Menlo Park, CA,
  February 1993.
\newblock Also appears in Tutorial Notes, {\em Formal Methods Europe '93:
  Industrial-Strength Formal Methods}, pages 357--406, Odense, Denmark, April
  1993.

\bibitem{PVS96:CAV}
S.~Owre, S.~Rajan, J.M. Rushby, N.~Shankar, and M.K. Srivas.
\newblock {PVS}: Combining specification, proof checking, and model checking.
\newblock In Rajeev Alur and Thomas~A. Henzinger, editors, {\em Computer-Aided
  Verification, CAV '96}, volume 1102 of {\em Lecture Notes in Computer
  Science}, pages 411--414, New Brunswick, NJ, July/August 1996.
  Springer-Verlag.

\bibitem{PVS-CADE92}
S.~Owre, J.~M. Rushby, and N.~Shankar.
\newblock {PVS}: A prototype verification system.
\newblock In Deepak Kapur, editor, {\em 11th International Conference on
  Automated Deduction (CADE)}, volume 607 of {\em Lecture Notes in Artificial
  Intelligence}, pages 748--752, Saratoga, NY, June 1992. Springer-Verlag.

\bibitem{Shankar96:FMCAD}
N.~Shankar.
\newblock {PVS}: Combining specification, proof checking, and model checking.
\newblock In Mandayam Srivas and Albert Camilleri, editors, {\em Formal Methods
  in Computer-Aided Design (FMCAD '96)}, volume 1166 of {\em Lecture Notes in
  Computer Science}, pages 257--264, Palo Alto, CA, November 1996.
  Springer-Verlag.

\bibitem{Owre-etal98:FM-TRENDS}
Sam Owre, John Rushby, N.~Shankar, and David Stringer-Calvert.
\newblock {PVS:} an experience report.
\newblock In Dieter Hutter, Werner Stephan, Paolo Traverso, and Markus Ullman,
  editors, {\em Applied Formal Methods---FM-Trends 98}, volume 1641 of {\em
  Lecture Notes in Computer Science}, pages 338--345, Boppard, Germany, October
  1998. Springer-Verlag.

\bibitem{PVS:language}
S.~Owre, N.~Shankar, J.~M. Rushby, and D.~W.~J. Stringer-Calvert.
\newblock {\em PVS Language Reference}.
\newblock Computer Science Laboratory, SRI International, Menlo Park, CA,
  September 1999.

\bibitem{PVS:prover}
N.~Shankar, S.~Owre, J.~M. Rushby, and D.~W.~J. Stringer-Calvert.
\newblock {\em PVS Prover Guide}.
\newblock Computer Science Laboratory, SRI International, Menlo Park, CA,
  September 1999.

\bibitem{PVS:userguide}
S.~Owre, N.~Shankar, J.~M. Rushby, and D.~W.~J. Stringer-Calvert.
\newblock {\em PVS System Guide}.
\newblock Computer Science Laboratory, SRI International, Menlo Park, CA,
  September 1999.

\bibitem{PVS-Semantics:TR}
Sam Owre and Natarajan Shankar.
\newblock The formal semantics of {PVS}.
\newblock Technical Report SRI-CSL-97-2, Computer Science Laboratory, SRI
  International, Menlo Park, CA, August 1997.

\bibitem{Owre95:prolegomena}
Sam Owre, John Rushby, Natarajan Shankar, and Friedrich von Henke.
\newblock Formal verification for fault-tolerant architectures: Prolegomena to
  the design of {PVS}.
\newblock {\em IEEE Transactions on Software Engineering}, 21(2):107--125,
  February 1995.

\bibitem{Rushby98:TSE}
John Rushby, Sam Owre, and N.~Shankar.
\newblock Subtypes for specifications: Predicate subtyping in {PVS}.
\newblock {\em IEEE Transactions on Software Engineering}, 24(9):709--720,
  September 1998.

\bibitem{Shankar&Owre:WADT99}
Natarajan Shankar and Sam Owre.
\newblock Principles and pragmatics of subtyping in {PVS}.
\newblock In Didier Bert, Christine Choppy, and Peter Mosses, editors, {\em
  Recent Trends in Algebraic Development Techniques, {WADT '99}}, volume 1827
  of {\em Lecture Notes in Computer Science}, pages 37--52, Toulouse, France,
  September 1999. Springer-Verlag.

\bibitem{Butler:PVS-tut}
Ricky~W. Butler.
\newblock An elementary tutorial on formal specification and verification using
  {PVS 2}.
\newblock NASA Technical Memorandum 108991, NASA Langley Research Center,
  Hampton, VA, June 1993.
\newblock 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.''.

\bibitem{WIFT-Tut}
Judy Crow, Sam Owre, John Rushby, Natarajan Shankar, and Mandayam Srivas.
\newblock A tutorial introduction to {PVS}.
\newblock Presented at WIFT '95: Workshop on Industrial-Strength Formal
  Specification Techniques, Boca Raton, Florida, April 1995.
\newblock Available, with specification files, at
  \url{http://www.csl.sri.com/wift-tutorial.html}.

\bibitem{Rushby&Stringer-Calvert95}
John Rushby and David W.~J. Stringer-Calvert.
\newblock A less elementary tutorial for the {PVS} specification and
  verification system.
\newblock Technical Report SRI-CSL-95-10, Computer Science Laboratory, SRI
  International, Menlo Park, CA, June 1995.
\newblock Revised, July 1996. Available, with specification files, at
  \url{http://www.csl.sri.com/csl-95-10.html}.

\bibitem{Owre94:TPCD}
S.~Owre, J.~M. Rushby, N.~Shankar, and M.~K. Srivas.
\newblock A tutorial on using {PVS} for hardware verification.
\newblock In Ramayya Kumar and Thomas Kropf, editors, {\em Theorem Provers in
  Circuit Design ({TPCD} '94)}, volume 910 of {\em Lecture Notes in Computer
  Science}, pages 258--279, Bad Herrenalb, Germany, September 1994.
  Springer-Verlag.

\bibitem{PVS-ADT:TR}
Sam Owre and Natarajan Shankar.
\newblock Abstract datatypes in {PVS}.
\newblock Technical Report SRI-CSL-93-9R, Computer Science Laboratory, SRI
  International, Menlo Park, CA, December 1993.
\newblock Extensively revised June 1997; Also available as NASA Contractor
  Report CR-97-206264.

\bibitem{Owre95:tables}
Sam Owre, John Rushby, and Natarajan Shankar.
\newblock Analyzing tabular and state-transition specifications in {PVS}.
\newblock Technical Report SRI-CSL-95-12, Computer Science Laboratory, SRI
  International, Menlo Park, CA, July 1995.
\newblock Available, with specification files, at
  \url{http://www.csl.sri.com/csl-95-12.html}. Also published as NASA
  Contractor Report 201729.

\bibitem{FORTE97-Tut}
John Rushby.
\newblock Specification, proof checking, and model checking for protocols and
  distributed systems with {PVS}.
\newblock Tutorial presented at {FORTE X/PSTV XVII '97}: Formal Description
  Techniques and Protocol Specification, Testing and Verification, November
  1997.
\newblock Available, with specification files, at
  \url{http://www.csl.sri.com/forte97.html}.

\bibitem{Rushby00:Movep2k}
John Rushby.
\newblock Theorem proving for verification.
\newblock In Franck Cassez, editor, {\em Modelling and Verification of Parallel
  Processes: MoVEP 2k}, Nantes, France, June 2000.
\newblock Tutorial presented at MoVEP: revised version to be published by
  Springer LNCS.

\bibitem{NASA-GB1}
Judith Crow et~al.
\newblock {\em NASA Formal Methods Specification and Verification Guidebook for
  Software and Computer Systems, Volume I: Planning and Technology Insertion}.
\newblock NASA Office of Safety and Mission Assurance, Washington, DC, 1995.
\newblock Available at \url{http://eis.jpl.nasa.gov/quality/Formal_Methods/}.

\bibitem{NASA-GB2}
Judith Crow et~al.
\newblock {\em NASA Formal Methods Specification and Verification Guidebook for
  Software and Computer Systems, Volume II: A Practitioner's Companion}.
\newblock NASA Office of Safety and Mission Assurance, Washington, DC, 1997.
\newblock Available at \url{http://eis.jpl.nasa.gov/quality/Formal_Methods/}.

\bibitem{Cyrluk&Srivas95:iccd}
David~A. Cyrluk and Mandayam~K. Srivas.
\newblock Theorem proving: Not an esoteric diversion, but the unifying
  framework for industrial verification.
\newblock In {\em International Conference on Computer Design: {VLSI} in
  Computers and Processors ({ICCD} '95)}, pages 538--544, Austin, TX, October
  1995. IEEE Computer Society.

\bibitem{Dill&Rushby96}
David~L. Dill and John Rushby.
\newblock Acceptance of formal methods: Lessons from hardware design.
\newblock {\em IEEE Computer}, 29(4):23--24, April 1996.
\newblock Part of~\cite{Saiedian96}.

\bibitem{Rushby92:repsa}
John Rushby.
\newblock Formal methods for dependable real-time systems.
\newblock In {\em International Symposium on Real-Time Embedded Processing for
  Space Applications}, pages 355--366, Les Saintes-Maries-de-la-Mer, France,
  November 1992. CNES, the French Space Agency.
\newblock Published by C\'{e}padu\`{e}s-\'{E}ditions, Toulouse, France.

\bibitem{Rushby95:ZUM}
John Rushby.
\newblock Mechanizing formal methods: Opportunities and challenges.
\newblock In Jonathan~P. Bowen and Michael~G. Hinchey, editors, {\em {ZUM} '95:
  The {Z} Formal Specification Notation; 9th International Conference of {Z}
  Users}, volume 967 of {\em Lecture Notes in Computer Science}, pages
  105--113, Limerick, Ireland, September 1995. Springer-Verlag.

\bibitem{Rushby96:CAV}
John Rushby.
\newblock Automated deduction and formal methods.
\newblock In Rajeev Alur and Thomas~A. Henzinger, editors, {\em Computer-Aided
  Verification, CAV '96}, volume 1102 of {\em Lecture Notes in Computer
  Science}, pages 169--183, New Brunswick, NJ, July/August 1996.
  Springer-Verlag.

\bibitem{Rushby96:FSTTCS}
John Rushby.
\newblock Mechanized formal methods: Progress and prospects.
\newblock In V.~Chandru and V.~Vinay, editors, {\em 16th Conference on the
  Foundations of Software Technology and Theoretical Computer Science}, volume
  1180 of {\em Lecture Notes in Computer Science}, pages 43--51, Hyderabad,
  India, December 1996. Springer-Verlag.

\bibitem{Rushby97:isre}
John Rushby.
\newblock Calculating with requirements.
\newblock In {\em 3rd IEEE International Symposium on Requirements
  Engineering}, pages 144--146, Annapolis, MD, January 1997. IEEE Computer
  Society.

\bibitem{Rushby:FM99}
John Rushby.
\newblock Mechanized formal methods: Where next?
\newblock In Jeannette Wing and Jim Woodcock, editors, {\em FM99: The World
  Congress in Formal Methods}, volume 1708 and 1709 of {\em Lecture Notes in
  Computer Science}, pages 48--51, Toulouse, France, September 1999.
  Springer-Verlag.
\newblock Pages 1--938 are in the first volume, 939--1872 in the second.

\bibitem{Shankar85}
N.~Shankar.
\newblock Towards mechanical metamathematics.
\newblock {\em Journal of Automated Reasoning}, 1(4):407--434, 1985.

\bibitem{Shankar:notes}
N.~Shankar.
\newblock Observations on the use of computers in proof checking.
\newblock {\em Notices of the American Mathematical Society}, 35(6):804--805,
  July/August 1988.

\bibitem{Shankar:book}
N.~Shankar.
\newblock {\em Metamathematics, Machines, and {G{\"o}del's} Proof}.
\newblock Cambridge Tracts in Theoretical Computer Science. Cambridge
  University Press, Cambridge, UK, 1994.

\bibitem{Shankar:FTRTFT96}
Natarajan Shankar.
\newblock Unifying verification paradigms.
\newblock In Bengt Jonsson and Joachim Parrow, editors, {\em Formal Techniques
  in Real-Time and Fault-Tolerant Systems}, volume 1135 of {\em Lecture Notes
  in Computer Science}, pages 22--39, Uppsala, Sweden, September 1996.
  Springer-Verlag.

\bibitem{Rushby:FAA-full}
John Rushby.
\newblock Formal methods and the certification of critical systems.
\newblock Technical Report SRI-CSL-93-7, Computer Science Laboratory, SRI
  International, Menlo Park, CA, December 1993.
\newblock 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.

\bibitem{Rushby94:Taxonomy}
John Rushby.
\newblock Critical system properties: Survey and taxonomy.
\newblock {\em Reliability Engineering and System Safety}, 43(2):189--219,
  1994.

\bibitem{Rushby:FAA-short}
John Rushby.
\newblock Formal methods and their role in the certification of critical
  systems.
\newblock Technical Report SRI-CSL-95-1, Computer Science Laboratory, SRI
  International, Menlo Park, CA, March 1995.
\newblock 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}.

\bibitem{Srivas97:chapter}
Mandayam Srivas, Harald Rue{\ss}, and David Cyrluk.
\newblock Hardware verification using {PVS}.
\newblock In Thomas Kropf, editor, {\em Formal Hardware Verification: Methods
  and Systems in Comparison}, volume 1287 of {\em Lecture Notes in Computer
  Science}, pages 156--205. Springer-Verlag, 1997.

\bibitem{Cyrluk96:DP}
David Cyrluk, Patrick Lincoln, and N.~Shankar.
\newblock On {Shostak's} decision procedure for combinations of theories.
\newblock In M.~A. McRobbie and J.~K. Slaney, editors, {\em Automated
  Deduction---{CADE-13}}, volume 1104 of {\em Lecture Notes in Artificial
  Intelligence}, pages 463--477, New Brunswick, NJ, July/August 1996.
  Springer-Verlag.

\bibitem{Cyrluk-etal97:CAV}
David Cyrluk, Harald Rue{\ss}, and Oliver M{\"o}ller.
\newblock An efficient decision procedure for the theory of fixed-sized
  bit-vectors.
\newblock In Orna Grumberg, editor, {\em Computer-Aided Verification, CAV '97},
  volume 1254 of {\em Lecture Notes in Computer Science}, pages 60--71, Haifa,
  Israel, June 1997. Springer-Verlag.

\bibitem{Cyrluk94:gtl}
D.~Cyrluk and P.~Narendran.
\newblock Ground temporal logic---a logic for hardware verification.
\newblock In David Dill, editor, {\em Computer-Aided Verification, CAV '94},
  volume 818 of {\em Lecture Notes in Computer Science}, pages 247--259,
  Stanford, CA, June 1994. Springer-Verlag.

\bibitem{Cyrluk94:TPCD}
D.~Cyrluk, S.~Rajan, N.~Shankar, and M.~K. Srivas.
\newblock Effective theorem proving for hardware verification.
\newblock In Ramayya Kumar and Thomas Kropf, editors, {\em Theorem Provers in
  Circuit Design ({TPCD} '94)}, volume 910 of {\em Lecture Notes in Computer
  Science}, pages 203--222, Bad Herrenalb, Germany, September 1994.
  Springer-Verlag.

\bibitem{Moeller98:FMCAD}
Oliver M{\"o}ller and Harald Rue{\ss}.
\newblock Solving bit-vector equations.
\newblock In Ganesh Gopalakrishnan and Phillip Windley, editors, {\em Formal
  Methods in Computer-Aided Design (FMCAD '98)}, volume 1522 of {\em Lecture
  Notes in Computer Science}, pages 36--48, Palo Alto, CA, November 1998.
  Springer-Verlag.

\bibitem{Tiwari-etal00:CADE}
Ashish Tiwari, Leo Bachmair, and Harald Rue{\ss}.
\newblock Rigid e-unification revisited.
\newblock In David McAllester, editor, {\em Automated Deduction---{CADE-17}},
  volume 1831 of {\em Lecture Notes in Artificial Intelligence}, pages
  220--234, Pittsburgh, PA, June 2000. Springer-Verlag.

\bibitem{Rajan95:CAV}
S.~Rajan, N.~Shankar, and M.K. Srivas.
\newblock An integration of model-checking with automated proof checking.
\newblock In Pierre Wolper, editor, {\em Computer-Aided Verification, CAV '95},
  volume 939 of {\em Lecture Notes in Computer Science}, pages 84--97, Liege,
  Belgium, June 1995. Springer-Verlag.

\bibitem{pvs-tables:tacas97}
Sam Owre, John Rushby, and N.~Shankar.
\newblock Integration in {PVS}: Tables, types, and model checking.
\newblock In Ed~Brinksma, editor, {\em Tools and Algorithms for the
  Construction and Analysis of Systems {(TACAS '97)}}, volume 1217 of {\em
  Lecture Notes in Computer Science}, pages 366--383, Enschede, The
  Netherlands, April 1997. Springer-Verlag.

\bibitem{Owre&Ruess00:CAV}
Sam Owre and Harald Rue{\ss}.
\newblock Integrating {WS1S} with {PVS}.
\newblock In E.~A. Emerson and A.~P. Sistla, editors, {\em Computer-Aided
  Verification, CAV '2000}, volume 1855 of {\em Lecture Notes in Computer
  Science}, pages 548--551, Chicago, IL, July 2000. Springer-Verlag.

\bibitem{Pfab98:tools}
Friedrich von Henke, Stephan Pfab, Harald Rue{\ss}, and Sam Owre.
\newblock Towards light-weight verification and heavy-weight testing.
\newblock In Rudolph Berghammer and Yassine Lakhnech, editors, {\em Tool
  Support for System Specification, Development, and Verification}, Advances in
  Computing Science, pages 189--200, Malente, Germany, June 1998.
  Springer-Verlag.
\newblock Proceedings published in May 1999.

\bibitem{vonHenke98:tphols}
Friedrich von Henke, Stephan Pfab, Holger Pfeifer, and Harald Rue{\ss}.
\newblock Case studies in meta-level theorem proving.
\newblock In Jim Grundy and Malcolm Newey, editors, {\em Theorem Proving in
  Higher Order Logics: 11th International Conference, {TPHOLs '98}}, volume
  1479 of {\em Lecture Notes in Computer Science}, pages 461--478, Canberra,
  Australia, September 1998. Springer-Verlag.

\bibitem{shankar99:eval}
N.~Shankar.
\newblock Efficiently executing {PVS}.
\newblock Project report, Computer Science Laboratory, SRI International, Menlo
  Park, CA, November 1999.
\newblock Available at \url{http://www.csl.sri.com/shankar/PVSeval.ps.gz}.

\bibitem{Bensalem96:CAV}
Saddek Bensalem, Yassine Lakhnech, and Hassen Sa{\"\i}di.
\newblock Powerful techniques for the automatic generation of invariants.
\newblock In Rajeev Alur and Thomas~A. Henzinger, editors, {\em Computer-Aided
  Verification, CAV '96}, volume 1102 of {\em Lecture Notes in Computer
  Science}, pages 323--335, New Brunswick, NJ, July/August 1996.
  Springer-Verlag.

\bibitem{Bensalem98:CAV}
Saddek Bensalem, Yassine Lakhnech, and Sam Owre.
\newblock Computing abstractions of infinite state systems compositionally and
  automatically.
\newblock In Alan~J. Hu and Moshe~Y. Vardi, editors, {\em Computer-Aided
  Verification, CAV '98}, volume 1427 of {\em Lecture Notes in Computer
  Science}, pages 319--331, Vancouver, Canada, June 1998. Springer-Verlag.

\bibitem{Abdulla:CAV99}
Parosh~Aziz Abdulla, Aurore Annichini, Saddek Bensalem, Ahmed Bouajjani, Peter
  Habermehl, and Yassine Lakhnech.
\newblock Verification of infinite-state systems by combining abstraction and
  reachability analysis.
\newblock In Nicolas Halbwachs and Doron Peled, editors, {\em Computer-Aided
  Verification, CAV '99}, volume 1633 of {\em Lecture Notes in Computer
  Science}, pages 146--159, Trento, Italy, July 1999. Springer-Verlag.

\bibitem{Rusu&Singerman99}
Vlad Rusu and Eli Singerman.
\newblock On proving safety properties by integrating static analysis, theorem
  proving and abstraction.
\newblock In W.~Rance Cleaveland, editor, {\em Tools and Algorithms for the
  Construction and Analysis of Systems {(TACAS '99)}}, volume 1579 of {\em
  Lecture Notes in Computer Science}, pages 178--192, Amsterdam, The
  Netherlands, March 1999. Springer-Verlag.

\bibitem{Graf96:CAV}
Susanne Graf and Hassen Sa{\"\i}di.
\newblock Verifying invariants using theorem proving.
\newblock In Rajeev Alur and Thomas~A. Henzinger, editors, {\em Computer-Aided
  Verification, CAV '96}, volume 1102 of {\em Lecture Notes in Computer
  Science}, pages 196--207, New Brunswick, NJ, July/August 1996.
  Springer-Verlag.

\bibitem{Saidi96}
Hassen Sa{\"\i}di.
\newblock A tool for proving invariance properties of concurrent systems
  automatically.
\newblock In {\em Tools and Algorithms for the Construction and Analysis of
  Systems {TACAS '96}}, volume 1055 of {\em Lecture Notes in Computer Science},
  pages 412--416, Passau, Germany, March 1996. Springer-Verlag.

\bibitem{Saidi97:CAV}
Hassen Sa{\"\i}di.
\newblock {The Invariant Checker}: Automated deductive verification of reactive
  systems.
\newblock In Orna Grumberg, editor, {\em Computer-Aided Verification, CAV '97},
  volume 1254 of {\em Lecture Notes in Computer Science}, pages 436--439,
  Haifa, Israel, June 1997. Springer-Verlag.

\bibitem{Saidi&Graf97:CAV}
Hassen Sa{\"\i}di and Susanne Graf.
\newblock Construction of abstract state graphs with {PVS}.
\newblock In Orna Grumberg, editor, {\em Computer-Aided Verification, CAV '97},
  volume 1254 of {\em Lecture Notes in Computer Science}, pages 72--83, Haifa,
  Israel, June 1997. Springer-Verlag.

\bibitem{Saidi97:LFM}
Hassen Sa{\"\i}di.
\newblock Automated deductive verification of parallel systems.
\newblock In C.~Michael Holloway and Kelly~J. Hayhurst, editors, {\em LFM' 97:
  Fourth NASA Langley Formal Methods Workshop}, NASA Conference Publication
  3356, pages 163--176, Hampton, VA, September 1997. NASA Langley Research
  Center.
\newblock Available at \url{http://atb-www.larc.nasa.gov/Lfm97/proceedings/}.

\bibitem{Saidi&Shankar:CAV99}
Hassen Sa{\"\i}di and N.~Shankar.
\newblock Abstract and model check while you prove.
\newblock In Nicolas Halbwachs and Doron Peled, editors, {\em Computer-Aided
  Verification, CAV '99}, volume 1633 of {\em Lecture Notes in Computer
  Science}, pages 443--454, Trento, Italy, July 1999. Springer-Verlag.

\bibitem{Saidi00:SAS}
Hassen Sa\"{\i}di.
\newblock Model checking guided abstraction and analysis.
\newblock In Jens Palsberg, editor, {\em Seventh International Static Analysis
  Symposium {(SAS'00)}}, volume 1824 of {\em Lecture Notes in Computer
  Science}, pages 377--396, Santa Barbara CA, June 2000. Springer-Verlag.

\bibitem{Shankar00:ASM}
Natarajan Shankar.
\newblock Symbolic analysis of transition systems.
\newblock In Yuri Gurevich, Phillip~W. Kutter, Martin Odersky, and Lothar
  Thiele, editors, {\em Abstract State Machines: Theory and Applications ({ASM}
  2000)}, number 1912 in Lecture Notes in Computer Science, pages 287--302,
  Monte Verit\`{a}, Switzerland, March 2000. Springer-Verlag.

\bibitem{Shankar00:CONCUR}
Natarajan Shankar.
\newblock Combining theorem proving and model checking through symbolic
  analysis.
\newblock In {\em {CONCUR 2000}: Concurrency Theory}, number 1877 in Lecture
  Notes in Computer Science, pages 1--16, State College, PA, August 2000.
  Springer-Verlag.

\bibitem{Bensalem98:InVeSt}
Saddek Bensalem, Yassine Lakhnech, and Sam Owre.
\newblock {InVeSt: A} tool for the verification of invariants.
\newblock In Alan~J. Hu and Moshe~Y. Vardi, editors, {\em Computer-Aided
  Verification, CAV '98}, volume 1427 of {\em Lecture Notes in Computer
  Science}, pages 505--510, Vancouver, Canada, June 1998. Springer-Verlag.

\bibitem{SALoverview00:LFM}
Saddek Bensalem, Vijay Ganesh, Yassine Lakhnech, C\'{e}sar Mu{\~{n}}oz, Sam
  Owre, Harald Rue{\ss}, John Rushby, Vlad Rusu, Hassen Sa{\"\i}di, N.~Shankar,
  Eli Singerman, and Ashish Tiwari.
\newblock An overview of {SAL}.
\newblock In C.~Michael Holloway, editor, {\em LFM 2000: Fifth NASA Langley
  Formal Methods Workshop}, pages 187--196, Hampton, VA, June 2000. NASA
  Langley Research Center.
\newblock Proceedings available at
  \url{http://shemesh.larc.nasa.gov/fm/Lfm2000/Proc/}.

\bibitem{Rushby98:ICFEM}
John Rushby.
\newblock Ubiquitous abstraction: A new approach for mechanized formal
  verification (extended abstract).
\newblock In John Staples, Michael~G. Hinchey, and Shaoying Liu, editors, {\em
  Second International Conference on Formal Engineering Methods (ICFEM '98)},
  pages 176--178, Brisbane, Australia, December 1998. IEEE Computer Society.

\bibitem{Rushby:SPIN99}
John Rushby.
\newblock Integrated formal verification: Using model checking with automated
  abstraction, invariant generation, and theorem proving.
\newblock In D.~Dams, R.~Gerth, S.~Leue, and M.~Massink, editors, {\em
  Theoretical and Practical Aspects of SPIN Model Checking: 5th and 6th
  International SPIN Workshops}, volume 1680 of {\em Lecture Notes in Computer
  Science}, pages 1--11, Trento, Italy, and Toulouse, France, July and
  September 1999. Springer-Verlag.

\bibitem{Rushby00:Forte}
John Rushby.
\newblock From refutation to verification.
\newblock In Tommaso Bolognesi and Diego Latella, editors, {\em Formal
  Description Techniques and Protocol Specification, Testing and Verification
  {FORTE XIII/PSTV XX 2000}}, pages 369--374, Pisa, Italy, October 2000. Kluwer
  Academic Publishers.

\bibitem{Rushby00:HASE}
John Rushby.
\newblock Disappearing formal methods.
\newblock In {\em High-Assurance Systems Engineering Symposium}, pages 95--96,
  Albuquerque, NM, November 2000. Association for Computing Machinery.

\bibitem{Young97:IC}
William~D. Young.
\newblock Comparing verification systems: {Interactive Consistency} in {ACL2}.
\newblock {\em IEEE Transactions on Software Engineering}, 23(4):214--223,
  April 1997.

\bibitem{Miner95:HOL}
Victor~A. {Carre{\~{n}}o} and Paul~S. Miner.
\newblock Specification of the {IEEE-854} floating-point standard in {HOL} and
  {PVS}.
\newblock In {\em {HOL95}: Eighth International Workshop on Higher-Order Logic
  Theorem Proving and Its Applications}, Aspen Grove, UT, September 1995.
\newblock Category B proceedings, available at
  \url{http://lal.cs.byu.edu/lal/hol95/Bprocs/indexB.html}.

\bibitem{Gordon95:PVS}
Mike Gordon.
\newblock Notes on {PVS} from a {HOL} perspective.
\newblock Available at \url{http://www.cl.cam.ac.uk/users/mjcg/PVS.html},
  August 1995.

\bibitem{Griffioen98:tphols}
David Griffioen and Marieke Huisman.
\newblock A comparison of {PVS} and {Isabelle/HOL}.
\newblock In Jim Grundy and Malcolm Newey, editors, {\em Theorem Proving in
  Higher Order Logics: 11th International Conference, {TPHOLs '98}}, volume
  1479 of {\em Lecture Notes in Computer Science}, pages 123--142, Canberra,
  Australia, September 1998. Springer-Verlag.

\bibitem{Groote-etal98:CONCUR}
Jan~Friso Groote, {c}ois~Monin Fran\, and Jaco van~de Pol.
\newblock Checking verifications of protocols and distributed systems by
  computer.
\newblock In Davide Sangiorgi and Robert de~Simone, editors, {\em {CONCUR'98}:
  Concurrency Theory}, volume 1466 of {\em Lecture Notes in Computer Science},
  pages 629--655, Nice, France, September 1998. Springer-Verlag.

\bibitem{Kern99:todaes}
Christoph Kern and Mark~R. Greenstreet.
\newblock Formal verification in hardware design: A survey.
\newblock {\em ACM Transactions on Design Automation of Electronic Systems
  (TODAES)}, 4(2):123--193, April 1999.

\bibitem{Rust98}
Heinrich Rust.
\newblock A {PVS} specification of an invoicing system.
\newblock In M.~Allemand, C.~Attiogb\'{e}, and H.~Habrias, editors, {\em
  Proceedings of an International Workshop on Specification Techniques and
  Formal Methods}, pages 51--65. University of Nantes, France, March 1998.
\newblock Available at
  \url{http://www.informatik.tu-cottbus.de/~rust/publications/a_pvs_specificat
  ion_of_an_invoicing_system.ps.gz}.

\bibitem{Wilding97:LFM}
Matthew Wilding.
\newblock Robust computer system proofs in {PVS}.
\newblock In C.~Michael Holloway and Kelly~J. Hayhurst, editors, {\em LFM' 97:
  Fourth NASA Langley Formal Methods Workshop}, NASA Conference Publication
  3356, pages 177--184, Hampton, VA, September 1997. NASA Langley Research
  Center.
\newblock Available at \url{http://atb-www.larc.nasa.gov/Lfm97/proceedings/}.

\bibitem{Droschl:IFMW99}
Georg Droschl.
\newblock On the integration of formal methods: Events and scenarios in {PVS}
  and {VDM}.
\newblock In {\em Proceedings, 3rd. Irish Workshop in Formal Methods}, Galway,
  Ireland, July 1999. Electronic Workshops in Computing
  (\url{http://ewic.org.uk/ewic/}).

\bibitem{Droschl:FM99}
Georg Droschl.
\newblock Analyzing the requirements of an access control using {VDMTools} and
  {PVS}.
\newblock In Jeannette Wing and Jim Woodcock, editors, {\em FM99: The World
  Congress in Formal Methods}, volume 1708 and 1709 of {\em Lecture Notes in
  Computer Science}, page 1807, Toulouse, France, September 1999.
  Springer-Verlag.
\newblock Pages 1--938 are in the first volume, 939--1872 in the second.

\bibitem{Merriam96}
Nicholas~A. Merriam and Michael~D. Harrison.
\newblock Evaluating the interfaces of three theorem proving assistants.
\newblock In F.~Bodart and J.~Vanderdonckt, editors, {\em Proceedings of the
  3rd International {Eurographics} Workshop on Design, Specification, and
  Verification of Interactive Systems}, 1996.

\bibitem{Archer&Heitmeyer97:TPHOLS}
Myla Archer and Constance Heitmeyer.
\newblock Human-style theorem proving using {PVS}.
\newblock In Elsa Gunter and Amy Felty, editors, {\em Theorem Proving in Higher
  Order Logics: 10th International Conference, {TPHOLs '97}}, volume 1275 of
  {\em Lecture Notes in Computer Science}, pages 33--48, Murray Hill, NJ,
  August 1997. Springer-Verlag.

\bibitem{Archer98:UITP}
Myla Archer, Constance Heitmeyer, and Steve Sims.
\newblock {TAME: A PVS} interface to simplify proofs for automata models.
\newblock In {\em User Interfaces for Theorem Provers}, Eindhoven, The
  Netherlands, July 1998.
\newblock Informal proceedings available at
  \url{http://www.win.tue.nl/cs/ipa/uitp/proceedings.html}.

\bibitem{Knight97:LFM}
John Knight, Colleen DeJong, Matthew Gibble, and Lu{\'\i}s Nakano.
\newblock Why are formal methods not used more widely?
\newblock In C.~Michael Holloway and Kelly~J. Hayhurst, editors, {\em LFM' 97:
  Fourth NASA Langley Formal Methods Workshop}, NASA Conference Publication
  3356, pages 1--12, Hampton, VA, September 1997. NASA Langley Research Center.
\newblock Available at \url{http://atb-www.larc.nasa.gov/Lfm97/proceedings/}.

\bibitem{Dutertre96}
Bruno Dutertre.
\newblock Elements of mathematical analysis in {PVS}.
\newblock In Joakim von Wright, Jim Grundy, and John Harrison, editors, {\em
  Theorem Proving in Higher Order Logics: 9th International Conference, {TPHOLs
  '96}}, volume 1125 of {\em Lecture Notes in Computer Science}, pages
  141--156, Turku, Finland, August 1996. Springer-Verlag.

\bibitem{Gottliebsen00:TPHOLS}
Hanne Gottliebsen.
\newblock Transcendental functions and continuity checking in {PVS}.
\newblock In Mark Aargaard and John Harrison, editors, {\em Theorem Proving in
  Higher Order Logics: 13th International Conference, {TPHOLs 2000}}, volume
  1869 of {\em Lecture Notes in Computer Science}, pages 197--214, Portland,
  OR, August 2000. Springer-Verlag.

\bibitem{Basten&Hooman99}
Twan Basten and Jozef Hooman.
\newblock Process algebra in {PVS}.
\newblock In W.~Rance Cleaveland, editor, {\em Tools and Algorithms for the
  Construction and Analysis of Systems {(TACAS '99)}}, volume 1579 of {\em
  Lecture Notes in Computer Science}, pages 270--284, Amsterdam, The
  Netherlands, March 1999. Springer-Verlag.

\bibitem{Schamschurko98}
Dmitri Schamschurko.
\newblock Modeling process calculi with {PVS}.
\newblock In B.~Jacobs, L.~Moss, H.~Reichel, and J.~Rutten, editors, {\em First
  Workshop on Coalgebraic Methods in Computer Science {(CMCS'98)}}, volume~11
  of {\em Electronic Notes in Theoretical Computer Science}, pages 197--214,
  Lisbon, Portugal, March 1998. Elsevier.
\newblock Available at
  \url{http://www.elsevier.nl/cas/tree/store/tcs/free/entcs/store/tcs11/tcs110
  11.ps}.

\bibitem{Griffioen98:CAV}
David Griffioen and Frits Vaandrager.
\newblock Normed simulations.
\newblock In Alan~J. Hu and Moshe~Y. Vardi, editors, {\em Computer-Aided
  Verification, CAV '98}, volume 1427 of {\em Lecture Notes in Computer
  Science}, pages 332--344, Vancouver, Canada, June 1998. Springer-Verlag.

\bibitem{Pnueli98:FTRTFT}
Amir Pnueli, N.~Shankar, and Eli Singerman.
\newblock Fair synchronous transition systems and their liveness proofs.
\newblock In {\em Formal Techniques in Real-Time and Fault-Tolerant Systems},
  volume 1486 of {\em Lecture Notes in Computer Science}, pages 198--209,
  Lyngby, Denmark, September 1998. Springer-Verlag.

\bibitem{Devillers-etal97}
M.~Devillers, D.~Griffioen, and O.~Mueller.
\newblock Possibly infinite sequences in theorem provers: A comparative study.
\newblock In Elsa Gunter and Amy Felty, editors, {\em Theorem Proving in Higher
  Order Logics: 10th International Conference, {TPHOLs '97}}, volume 1275 of
  {\em Lecture Notes in Computer Science}, pages 89--104, Murray Hill, NJ,
  August 1997. Springer-Verlag.

\bibitem{Hensel&Jacobs97}
Ulrich Hensel and Bart Jacobs.
\newblock Proof principles for datatypes with iterated recursion.
\newblock In Eugenio Moggi and Giuseppe Rosolini, editors, {\em Category Theory
  and Computer Science}, volume 1290 of {\em Lecture Notes in Computer
  Science}, pages 220--241, Santa Margherita Ligure, Italy, September 1997.
  Springer-Verlag.

\bibitem{Hensel98:JLC}
Ulrich Hensel and Bart Jacobs.
\newblock Coalgebraic theories of sequences in {PVS}.
\newblock {\em Journal of Logic and Computation}, 9(4):463--500, 1999.

\bibitem{Hensel-etal98}
Ulrich Hensel, Marieke Huisman, Bart Jacobs, and Hendrik Tews.
\newblock Reasoning about classes in object-oriented languages: Logical models
  and tools.
\newblock In Chris Hankin, editor, {\em Programming Languages and Systems: 7th
  European Symposium On Programming {(ESOP)}}, volume 1381 of {\em Lecture
  Notes in Computer Science}, pages 105--121, Lisbon, Portugal, March 1998.
  Springer-Verlag.

\bibitem{Huisman-etal99:ECOOP}
Marieke Huisman, Bart Jacobs, and Joachim van~den Berg.
\newblock A case study in class library verification: {Java's} vector class.
\newblock In A.~Moreira and D.~Demeyer, editors, {\em Object-Oriented
  Technology: ECOOP'99 Workshop Reader}, volume 1743 of {\em Lecture Notes in
  Computer Science}, pages 109---110, Lisbon, Portugal, June 1999.
  Springer-Verlag.

\bibitem{Jacobs98:OOPSLA}
Bart Jacobs, Joachim van~den Berg, Marieke Huisman, Martijn van Berkum, Ulrich
  Hensel, and Hendrick Tews.
\newblock Reasoning about {Java} classes.
\newblock In {\em Proceedings, Object-Oriented Programming Systems, Languages
  and Applications (OOPSLA'98)}, pages 329--340, Vancouver, Canada, October
  1998. Association for Computing Machinery.
\newblock Proceedings issued as ACM SIGPLAN Notices Vol.~33, No.~10, October
  1998.

\bibitem{Huisman&Jacobs00:TPHOLS}
Marieke Huisman and Bart Jacobs.
\newblock Inheritance in higher order logic: Modeling and reasoning.
\newblock In Mark Aargaard and John Harrison, editors, {\em Theorem Proving in
  Higher Order Logics: 13th International Conference, {TPHOLs 2000}}, volume
  1869 of {\em Lecture Notes in Computer Science}, pages 301--319, Portland,
  OR, August 2000. Springer-Verlag.

\bibitem{Huisman:PhD}
Marieke Huisman.
\newblock {\em Java Program Verification in {Higher}-Order Logic with {PVS} and
  {Isabelle}}.
\newblock PhD thesis, University of Nijmegen, The Netherlands, 2001.

\bibitem{Huisman&Jacobs00:FASE}
Marieke Huisman and Bart Jacobs.
\newblock Java program verfication via a hoare logic with abrupt termination.
\newblock In Tom Maibaum, editor, {\em Fundamental Approaches to Software
  Engineering, {FASE} 2000}, number 1783 in Lecture Notes in Computer Science,
  pages 284--303, Berlin, Germany, March/April 2000. Springer-Verlag.

\bibitem{vandenBerg-etal00:WADT}
Joachim van~den Berg, Marieke Huisman, Bart Jacobs, and Erik Poll.
\newblock A type-theoretic memory model for verification of sequential {Java}
  programs.
\newblock In Didier Bert, Christine Choppy, and Peter Mosses, editors, {\em
  Recent Trends in Algebraic Development Techniques, {WADT '99}}, number 1827
  in Lecture Notes in Computer Science, pages 1--21, Toulouse, France,
  September 1999. Springer-Verlag.

\bibitem{Lincoln&Rushby93:CAV}
Patrick Lincoln and John Rushby.
\newblock Formal verification of an algorithm for interactive consistency under
  a hybrid fault model.
\newblock In Costas Courcoubetis, editor, {\em Computer-Aided Verification, CAV
  '93}, volume 697 of {\em Lecture Notes in Computer Science}, pages 292--304,
  Elounda, Greece, June/July 1993. Springer-Verlag.

\bibitem{Lincoln&Rushby93:FTCS}
Patrick Lincoln and John Rushby.
\newblock A formally verified algorithm for interactive consistency under a
  hybrid fault model.
\newblock In {\em Fault Tolerant Computing Symposium 23}, pages 402--411,
  Toulouse, France, June 1993. IEEE Computer Society.
\newblock Reprinted in~\cite[pp.\ 438--447]{FTCS-highlights}.

\bibitem{Lincoln&Rushby94:FTP}
Patrick Lincoln and John Rushby.
\newblock Formal verification of an interactive consistency algorithm for the
  {Draper FTP} architecture under a hybrid fault model.
\newblock In {\em COMPASS '94 (Proceedings of the Ninth Annual Conference on
  Computer Assurance)}, pages 107--120, Gaithersburg, MD, June 1994. IEEE
  Washington Section.

\bibitem{Pfeifer99:DCCA}
Holger Pfeifer, Detlef Schwier, and Friedrich~W. von Henke.
\newblock Formal verification for time-triggered clock synchronization.
\newblock In Charles~B. Weinstock and John Rushby, editors, {\em Dependable
  Computing for Critical Applications---7}, volume~12 of {\em Dependable
  Computing and Fault Tolerant Systems}, pages 207--226, San Jose, CA, January
  1999. IEEE Computer Society.

\bibitem{Pfeifer00:FORTE}
Holger Pfeifer.
\newblock Formal verification of the {TTA} group membership algorithm.
\newblock In Tommaso Bolognesi and Diego Latella, editors, {\em Formal
  Description Techniques and Protocol Specification, Testing and Verification
  {FORTE XIII/PSTV XX 2000}}, pages 3--18, Pisa, Italy, October 2000. Kluwer
  Academic Publishers.

\bibitem{Rushby99:TSE}
John Rushby.
\newblock Systematic formal verification for fault-tolerant time-triggered
  algorithms.
\newblock {\em IEEE Transactions on Software Engineering}, 25(5):651--660,
  September/October 1999.

\bibitem{Rushby00:CAV}
John Rushby.
\newblock Verification diagrams revisited: Disjunctive invariants for easy
  verification.
\newblock In E.~A. Emerson and A.~P. Sistla, editors, {\em Computer-Aided
  Verification, CAV '2000}, volume 1855 of {\em Lecture Notes in Computer
  Science}, pages 508--520, Chicago, IL, July 2000. Springer-Verlag.

\bibitem{Schwier98:FTRTFT}
D.~Schwier and F.~von Henke.
\newblock Mechanical verification of clock synchronization algorithms.
\newblock In {\em Formal Techniques in Real-Time and Fault-Tolerant Systems},
  volume 1486 of {\em Lecture Notes in Computer Science}, pages 262--271,
  Lyngby, Denmark, September 1998. Springer-Verlag.

\bibitem{WalterLincolnSuri97}
Chris~J. Walter, Patrick Lincoln, and Neeraj Suri.
\newblock Formally verified on-line diagnosis.
\newblock {\em IEEE Transactions on Software Engineering}, 23(11):684--721,
  November 1997.

\bibitem{DiVito:partitioningCR}
Ben~L. {Di Vito}.
\newblock A formal model of partitioning for integrated modular avionics.
\newblock NASA Contractor Report CR-1998-208703, NASA Langley Research Center,
  August 1998.

\bibitem{diVito99:DCCA}
Ben~L. {Di Vito}.
\newblock A model of cooperative noninterference for integrated modular
  avionics.
\newblock In Charles~B. Weinstock and John Rushby, editors, {\em Dependable
  Computing for Critical Applications---7}, volume~12 of {\em Dependable
  Computing and Fault Tolerant Systems}, pages 269--286, San Jose, CA, January
  1999. IEEE Computer Society.

\bibitem{Wilding99:DCCA}
Matthew~M. Wilding, David~S. Hardin, and David~A. Greve.
\newblock Invariant performance: A statement of task isolation useful for
  embedded application integration.
\newblock In Charles~B. Weinstock and John Rushby, editors, {\em Dependable
  Computing for Critical Applications---7}, volume~12 of {\em Dependable
  Computing and Fault Tolerant Systems}, pages 287--300, San Jose, CA, January
  1999. IEEE Computer Society.

\bibitem{Butler96:rqts}
Ricky~W. Butler.
\newblock An introduction to requirements capture using {PVS}: Specification of
  a simple autopilot.
\newblock NASA Technical Memorandum 110255, NASA Langley Research Center,
  Hampton, VA, May 1996.

\bibitem{Dutertre&Stavridou97}
Bruno Dutertre and Victoria Stavridou.
\newblock Formal requirements analysis of an avionics control system.
\newblock {\em IEEE Transactions on Software Engineering}, 23(5):267--278, May
  1997.

\bibitem{Dutertre97:LFM}
Bruno Dutertre and Victoria Stavridou.
\newblock Requirements analysis of real-time control systems using {PVS}.
\newblock In C.~Michael Holloway and Kelly~J. Hayhurst, editors, {\em LFM' 97:
  Fourth NASA Langley Formal Methods Workshop}, NASA Conference Publication
  3356, pages 65--74, Hampton, VA, September 1997. NASA Langley Research
  Center.
\newblock Available at \url{http://atb-www.larc.nasa.gov/Lfm97/proceedings/}.

\bibitem{Crow&DiVito98:tosem}
Judith Crow and Ben~L. {Di Vito}.
\newblock Formalizing {Space Shuttle} software requirements: Four case studies.
\newblock {\em ACM Transactions on Software Engineering and Methodology},
  7(3):296--332, July 1998.

\bibitem{Easterbrook-etal98}
Steve Easterbrook, Robyn Lutz, Richard Covington, John Kelly, Yoko Ampo, and
  David Hamilton.
\newblock Experiences using lightweight formal methods for requirements
  modeling.
\newblock {\em IEEE Transactions on Software Engineering}, 24(1):4--14, January
  1998.

\bibitem{HAC-study}
Larry~W. Roberts and Mike Beims.
\newblock Using formal methods to assist in the requirements analysis of the
  {Space Shuttle HAC Change Request (CR 90960E)}.
\newblock Technical Report JSC-27599, NASA Johnson Space Center, Houston, TX,
  September 1996.

\bibitem{DiVito96}
Ben~L. {Di Vito}.
\newblock Formalizing new navigation requirements for {NASA's Space Shuttle}.
\newblock In {\em Formal Methods Europe {FME '96}}, volume 1051 of {\em Lecture
  Notes in Computer Science}, pages 160--178, Oxford, UK, March 1996.
  Springer-Verlag.

\bibitem{DiVito00:STTT}
Ben~L. {Di Vito}.
\newblock High-automation proofs for properties of requirements models.
\newblock {\em Software Tools for Technology Transfer}, 3(1), 2000.
\newblock To appear; available at
  \url{http://shemesh.larc.nasa.gov/people/bld/ftp/sttt-bld.ps}.

\bibitem{GPS-study}
Ben~L. {Di Vito} and Larry~W. Roberts.
\newblock Using formal methods to assist in the requirements analysis of the
  {Space Shuttle GPS Change Request}.
\newblock NASA Contractor Report 4752, NASA Langley Research Center, August
  1996.

\bibitem{Hamilton-etal95}
David Hamilton, Rick Covington, and John Kelly.
\newblock Experiences in applying formal methods to the analysis of software
  and system requirements.
\newblock In {\em WIFT '95: Workshop on Industrial-Strength Formal
  Specification Techniques}, pages 30--43, Boca Raton, FL, 1995. IEEE Computer
  Society.

\bibitem{Hamilton-etal95-2}
David Hamilton, Rick Covington, and Alice Lee.
\newblock An experience report on requirements reliability engineering using
  formal methods.
\newblock In {\em Sixth International Conference on Software Reliability
  Engineering, {ISSRE '95}}, pages 52--57, Toulouse, France, 1995. IEEE
  Computer Society.

\bibitem{Ampo&Lutz95}
Yoko Ampo and Robyn Lutz.
\newblock Evaluation of software safety analysis using formal methods.
\newblock In {\em Workshop for Foundation of Software Engineering {(FOSE)}},
  Hamana-Ko, Japan, December 1995.
\newblock In Japanese.

\bibitem{Lutz&Ampo94}
Robyn Lutz and Yoko Ampo.
\newblock Experience report: Using formal methods for requirements analysis of
  critical spacecraft software.
\newblock In {\em Proceedings of the 19th Annual Software Engineering
  Workshop}, pages 231--248, Greenbelt, MD, December 1994. NASA Goddard Space
  Flight Center.

\bibitem{Lutz97:LFM}
Robyn Lutz.
\newblock Reuse of a formal model for requirements validation.
\newblock In C.~Michael Holloway and Kelly~J. Hayhurst, editors, {\em LFM' 97:
  Fourth NASA Langley Formal Methods Workshop}, NASA Conference Publication
  3356, pages 75--86, Hampton, VA, September 1997. NASA Langley Research
  Center.
\newblock Available at \url{http://atb-www.larc.nasa.gov/Lfm97/proceedings/}.

\bibitem{Carreno&Munoz00:TPHOLS}
Victor Carre{\~{n}}o and C\'{e}sar Mu{\~{n}}oz.
\newblock Aircraft trajectory modeling and alerting algorithm verification.
\newblock In Mark Aargaard and John Harrison, editors, {\em Theorem Proving in
  Higher Order Logics: 13th International Conference, {TPHOLs 2000}}, volume
  1869 of {\em Lecture Notes in Computer Science}, pages 90--105, Portland, OR,
  August 2000. Springer-Verlag.

\bibitem{Carreno&Munoz00:DASC}
Victor Carre{\~{n}}o and C\'{e}sar Mu{\~{n}}oz.
\newblock Formal analysis of parallel landing scenarios.
\newblock In {\em 19th AIAA/IEEE Digital Avionics Systems Conference},
  Philadelphia, PA, October 2000.

\bibitem{Lawford-etal00:AMAST}
Mark Lawford, Jeff McDougall, Peter Froebel, and Greg Moum.
\newblock Practical application of functional and relational methods for the
  specification and verification of safety critical software.
\newblock In Teodor Rus, editor, {\em Algebraic Methodology and Software
  Technology, {AMAST} 2000}, volume 1816 of {\em Lecture Notes in Computer
  Science}, pages 73--88, Iowa City, IA, May 2000. Springer-Verlag.

\bibitem{Koo-etal99}
S.~Koo, H.~Son, and P.~Seong.
\newblock Mathematical verification of a nuclear power plant protection system
  function with combined {CPN} and {PVS}.
\newblock {\em Journal of the Korean Nuclear Society}, 31:157--171, April 1999.

\bibitem{vandePol98}
Jaco van~de Pol, Jozef Hooman, and Edwin de~Jong.
\newblock Formal requirements specification for command and control systems.
\newblock In {\em Engineering of Computer Based Systems {(ECBS)}}, pages
  37--44, Jerusalem, Israel, March--April 1998. IEEE Computer Society.
\newblock Available at \url{http://www.win.tue.nl/cs/tt/hooman/ECBS98.html}.

\bibitem{Dean97}
Drew Dean.
\newblock Static typing with dynamic linking.
\newblock In {\em Fourth ACM Conference on Computer and Communications
  Security}, pages 18--27, Zurich, Switzerland, April 1997. Association for
  Computing Machinery.

\bibitem{Hoffman98:CAV}
John Hoffman and Charlie Payne.
\newblock A formal experience at {Secure Computing Corporation}.
\newblock In Alan~J. Hu and Moshe~Y. Vardi, editors, {\em Computer-Aided
  Verification, CAV '98}, volume 1427 of {\em Lecture Notes in Computer
  Science}, pages 49--56, Vancouver, Canada, June 1998. Springer-Verlag.

\bibitem{Peri96}
Ramesh~V. Peri, William~A. Wulf, and Darrell~M. Kienzle.
\newblock A logic of composition for information flow predicates.
\newblock In {\em 9th Computer Security Foundations Workshop}, pages 82--94,
  Kenmare, Ireland, June 1996. IEEE Computer Society.

\bibitem{Dieckman98}
Darryl Dieckman, Perry Alexander, and Philip~A. Wilsey.
\newblock {ActiveSPEC}: A framework for the specification and verification of
  active network services and security policies.
\newblock In Nevin Heintze and Jeannette Wing, editors, {\em Workshop on Formal
  Methods and Security Protocols}, Indianapolis, IN, June 1998.
\newblock Informal proceedings available at
  \url{http://www.cs.bell-labs.com/who/nch/fmsp/program.html}.

\bibitem{Dutertre&Schneider97}
Bruno Dutertre and Steve Schneider.
\newblock Embedding {CSP} in {PVS}. an application to authentication protocols.
\newblock In Elsa Gunter and Amy Felty, editors, {\em Theorem Proving in Higher
  Order Logics: 10th International Conference, {TPHOLs '97}}, volume 1275 of
  {\em Lecture Notes in Computer Science}, pages 121--136, Murray Hill, NJ,
  August 1997. Springer-Verlag.

\bibitem{Millen:FMSP99}
Jonathan~K. Millen.
\newblock A necessarily parallel attack.
\newblock In Nevin Heintze and Edmund Clarke, editors, {\em Workshop on Formal
  Methods and Security Protocols, Part of the Federated Logic Conference},
  Trento, Italy, July 1999.

\bibitem{Monniaux99:CSFW}
David Monniaux.
\newblock Decision procedures for the analysis of cryptographic protocols by
  logics of belief.
\newblock In {\em 12th Computer Security Foundations Workshop}, pages 44--54,
  Mordano, Italy, June 1999. IEEE Computer Society.

\bibitem{Ruess&Millen00:FMCS}
Harald Rue{\ss} and Jonathan Millen.
\newblock Local secrecy for state-based models.
\newblock In {\em Formal Methods and Computer Security (FMCS)}, Chicago, IL,
  July 2000.

\bibitem{Gopi98:FSTTCS}
N.S. Pendharkar and K.~Gopinath.
\newblock Formal verification of an {O.S.} submodule.
\newblock In V.~Arvind and R.~Ramanujin, editors, {\em 18th Conference on the
  Foundations of Software Technology and Theoretical Computer Science}, volume
  1530 of {\em Lecture Notes in Computer Science}, pages 197--208, Madras,
  India, December 1998. Springer-Verlag.

\bibitem{Couturier98:CAV}
Rapha\"{e}l Couturier and Dominique M\'{e}ry.
\newblock An experiment in parallelizing an application using formal methods.
\newblock In Alan~J. Hu and Moshe~Y. Vardi, editors, {\em Computer-Aided
  Verification, CAV '98}, volume 1427 of {\em Lecture Notes in Computer
  Science}, pages 345--356, Vancouver, Canada, June 1998. Springer-Verlag.

\bibitem{Chkliaev99}
Dmitri Chkliaev, Jozef Hooman, and Peter van~der Stok.
\newblock Mechanical verification of a non-blocking atomic commitment protocol.
\newblock In {\em International Workshop on Distributed System Validation and
  Verification (DSVV'2000)}, pages E96--E103, Taipei, Taiwan, April 2000.

\bibitem{Chkliaev99:AE}
Dmitri Chkliaev, Jozef Hooman, and Peter van~der Stok.
\newblock Serializability preserving extensions of concurrency control
  protocols.
\newblock In D.~Bj{\o}rner, M.~Broy, and A.V. Zamulin, editors, {\em Third
  International {Andrei Ershov} Memorial Conference: Perspectives of System
  Informatics, {PSI'99}}, volume 1755 of {\em Lecture Notes in Computer
  Science}, pages 180--193, Novosibirsk, Russia, July 1999. Springer-Verlag.

\bibitem{Chkliaev00:ICFEM}
Dmitri Chkliaev, Jozef Hooman, and Peter van~der Stok.
\newblock Mechanical verification of transaction processing systems.
\newblock In {\em Third International Conference on Formal Engineering Methods
  (ICFEM 2000)}, pages 89--97, York, England, November 200. IEEE Computer
  Society.

\bibitem{Couturier98:IFMW}
Rapha\"{e}l Couturier.
\newblock Formal engineering of the bitonic sort using {PVS}.
\newblock In {\em Proceedings, 2nd. Irish Workshop in Formal Methods}, Cork,
  Ireland, July 1998. Electronic Workshops in Computing
  (\url{http://ewic.org.uk/ewic/}).

\bibitem{Devillers00:FMSD}
Marco Devillers, David Griffioen, Judi Romijn, and Frits Vaandrager.
\newblock Verification of a leader election protocol: Formal methods applied to
  {IEEE 1394}.
\newblock {\em Formal Methods in Systems Design}, 16(3):307--320, June 2000.

\bibitem{Glusman&Katz:CAV99}
Marcelo Glusman and Shmuel Katz.
\newblock Mechanizing proofs of computation equivalence.
\newblock In Nicolas Halbwachs and Doron Peled, editors, {\em Computer-Aided
  Verification, CAV '99}, volume 1633 of {\em Lecture Notes in Computer
  Science}, pages 354--367, Trento, Italy, July 1999. Springer-Verlag.

\bibitem{Havelund:FMPPTA99}
Klaus Havelund.
\newblock Mechanical verification of a garbage collector.
\newblock In Jos\'{e} Rolim et~al., editors, {\em Parallel and Distributed
  Processing (Combined Proceedings of 11 Workshops)}, volume 1586 of {\em
  Lecture Notes in Computer Science}, pages 1258--1283, San Juan, Puerto Rico,
  April 1999. Springer-Verlag.
\newblock Presented at the Workshop on Formal Methods for Parallel Programming:
  Theory and Applications {(FMPPTA)}.

\bibitem{Hooman98:EAS}
Jozef Hooman.
\newblock Formal verification of the binary exponential backoff protocol.
\newblock {\em Proceedings of the Estonian Academy of Sciences (Special issue
  on the 9th Nordic Workshop on Programming Theory)}, 4(2):89--105, 1998.
\newblock Also available at \url{http://www.win.tue.nl/cs/tt/hooman/BEB.html}.

\bibitem{Jackson98:tphols}
Paul Jackson.
\newblock Verifying a garbage collection algorithm.
\newblock In Jim Grundy and Malcolm Newey, editors, {\em Theorem Proving in
  Higher Order Logics: 11th International Conference, {TPHOLs '98}}, volume
  1479 of {\em Lecture Notes in Computer Science}, pages 225--244, Canberra,
  Australia, September 1998. Springer-Verlag.

\bibitem{Mokkedem00:FMSD}
Abdel Mokkedem, Ravi~M. Hosabettu, Michael~D. Jones, and Ganesh~C.
  Gopalakrishnan.
\newblock Formalization and analysis of a solution to the {PCI} 2.1 bus
  transaction ordering problem.
\newblock {\em Formal Methods in Systems Design}, 16(1):93--119, January 2000.

\bibitem{Penix98:fmsp}
John Penix, Dale Martin, Peter Frey, Radharamanan Radhakrishnan, Perry
  Alexander, and Phillip~A. Wilsey.
\newblock Experiences in verifying parallel simulation algorithms.
\newblock In Mark Ardis, editor, {\em Second Workshop on Formal Methods in
  Software Practice (FMSP '98)}, pages 16--23, Clearwater Beach, FL, March
  1998. Association for Computing Machinery.

\bibitem{Umamageswaran98:JSA}
Kothanda Umamageswaran, Krishnan Subramani, Philip~A. Wilsey, and Perry
  Alexander.
\newblock Formal verification and empirical analysis of rollback relaxation.
\newblock {\em Journal of Systems Architecture (formerly published as
  Microprocessing and Microprogramming: the Euromicro Journal)},
  44(6--7):473--495, March 1998.

\bibitem{Alagar-etal99:RTAS}
V.~S. Alagar, D.~Muthiayen, and F.~Pompeo.
\newblock From behavioral specification to axiomatic description of real-time
  reactive systems.
\newblock In {\em Fifth IEEE Real-Time Technology and Applications Symposium,
  Work-In-Progress Session}, Vancouver, British Columbia, Canada, June 1999.
  IEEE Computer Society.
\newblock Available at
  \url{http://www.cs.concordia.ca/~faculty/manas/rtas99wip/}.

\bibitem{Alborghetti97:FSE}
Andren Alborghetti, Angelo Gargantini, and Angelo Morzenti.
\newblock Providing automated support to deductive analysis of time critical
  systems.
\newblock In Mehdi Jazayeri and Helmut Schauer, editors, {\em Software
  Engineering---ESEC/FSE '97: Sixth European Software Engineering Conference
  and Fifth ACM SIGSOFT Symposium on the Foundations of Software Engineering},
  volume 1301 of {\em Lecture Notes in Computer Science}, pages 211--226,
  Zurich, Switzerland, September 1997. Springer-Verlag.

\bibitem{Archer&Heitmeyer96}
Myla Archer and Constance Heitmeyer.
\newblock Mechanical verification of timed automata: A case study.
\newblock In {\em IEEE Real-Time Technology and Applications Symposium
  (RTAS'96)}, pages 192--203, Brookline, MA, June 1996. IEEE Computer Society.

\bibitem{AHrtssWIP96}
M.~Archer and C.~Heitmeyer.
\newblock {TAME}: A specialized specification and verification system for timed
  automata.
\newblock In Azer Bestavros, editor, {\em Work In Progress (WIP) Proceedings of
  the 17th IEEE Real-Time Systems Symposium (RTSS'96)}, pages 3--6, Washington,
  DC, December 1996.
\newblock The WIP Proceedings is available at
  \url{http://www.cs.bu.edu/pub/ieee-rts/rtss96/wip/proceedings}.

\bibitem{Bun96:ASCI}
Leon Bun.
\newblock Checking properties of {ASTRAL} specifications with {PVS}.
\newblock In {\em Proceedings of 2nd Annual Conference of the Advanced School
  for Computing and Imaging {(ASCI'96)}}, pages 102--107, Lommel, Belgium, June
  1996.
\newblock Available at
  \url{http://sepc.twi.tudelft.nl/~leonbun/papers/asci96.ps}.

\bibitem{Bun97:ASCI}
Leon Bun.
\newblock Embedding {Astral} in {PVS}.
\newblock In {\em Proceedings of 3rd Annual Conference of the Advanced School
  for Computing and Imaging {(ASCI'97)}}, pages 130--136, Lommel, Belgium, June
  1997.
\newblock Available at
  \url{http://sepc.twi.tudelft.nl/~leonbun/papers/asci97.ps}.

\bibitem{deBoer96:ftrtft}
F.~S. de~Boer, H.~Tej, W.-P. de~Roever, and M.~van Hulst.
\newblock Compositionality in real-time shared variable concurrency.
\newblock In Bengt Jonsson and Joachim Parrow, editors, {\em Formal Techniques
  in Real-Time and Fault-Tolerant Systems}, volume 1135 of {\em Lecture Notes
  in Computer Science}, pages 420--439, Uppsala, Sweden, September 1996.
  Springer-Verlag.

\bibitem{DuBois97:isre}
Philippe~Du Bois, Eric Dubois, and Jean-Marc Zeippen.
\newblock On the use of a formal {RE} language: The generalized railroad
  crossing problem.
\newblock In {\em 3rd IEEE International Symposium on Requirements
  Engineering}, pages 128--137, Annapolis, MD, January 1997. IEEE Computer
  Society.

\bibitem{dutertre99b}
Bruno Dutertre.
\newblock The {Priority Ceiling Protocol}: Formalization and analysis using
  {PVS}.
\newblock Technical report, System Design Laboratory, SRI International, Menlo
  Park, CA, October 1999.
\newblock Available at
  \url{http://www.sdl.sri.com/dsa/publis/prio-ceiling.html}.

\bibitem{Dutertre&Stavridou00:DASC}
Bruno Dutertre and Victoria Stavridou.
\newblock Formal analysis for realtime scheduling.
\newblock In {\em 19th AIAA/IEEE Digital Avionics Systems Conference},
  Philadelphia, PA, October 2000.

\bibitem{Dutertre00:RTSS}
Bruno Dutertre.
\newblock Formal analysis of the priority ceiling protocol.
\newblock In {\em Real Time Systems Symposium}, Orlando, FL, December 2000.
  IEEE Computer Society.
\newblock To appear.

\bibitem{Fowler&Wellings96}
Simon Fowler and Andy Wellings.
\newblock Formal analysis of a real-time kernel specification.
\newblock In Bengt Jonsson and Joachim Parrow, editors, {\em Formal Techniques
  in Real-Time and Fault-Tolerant Systems}, volume 1135 of {\em Lecture Notes
  in Computer Science}, pages 440--458, Uppsala, Sweden, September 1996.
  Springer-Verlag.

\bibitem{Fowler97:RTSS}
Simon Fowler and Andy Wellings.
\newblock Formal development of a real-time kernel.
\newblock In {\em Real Time Systems Symposium}, pages 220--229, San Francisco,
  CA, December 1997. IEEE Computer Society.

\bibitem{Hooman94}
Jozef Hooman.
\newblock Correctness of real time systems by construction.
\newblock In H.~Langmaack, W.-P. {de Roever}, and J.~Vytopil, editors, {\em
  Formal Techniques in Real-Time and Fault-Tolerant Systems}, volume 863 of
  {\em Lecture Notes in Computer Science}, pages 19--40, L\"{u}beck, Germany,
  September 1994. Springer-Verlag.

\bibitem{Hooman96:RPC}
Jozef Hooman.
\newblock Using {PVS} for an assertional verification of the {RPC-Memory}
  specification problem.
\newblock In Manfred Broy, Stephan Merz, and Katharina Spies, editors, {\em
  Formal Systems Specification: The {RPC-Memory} Specification Case Study},
  volume 1169 of {\em Lecture Notes in Computer Science}, pages 275--304.
  Springer-Verlag, 1996.

\bibitem{Hooman97:AMAST}
Jozef Hooman.
\newblock Verification of distributed real-time and fault-tolerant protocols.
\newblock In Michael Johnson, editor, {\em Algebraic Methodology and Software
  Technology, {AMAST}'97}, volume 1349 of {\em Lecture Notes in Computer
  Science}, pages 261--275, Sydney, Australia, December 1997. Springer-Verlag.

\bibitem{Hooman97:compos}
Jozef Hooman.
\newblock Compositional verification of real-time applications.
\newblock In Willem-Paul de~Roever, Hans Langmaack, and Amir Pnueli, editors,
  {\em Compositionality: The Significant Difference (Revised lectures from
  International Symposium {COMPOS'97})}, volume 1536 of {\em Lecture Notes in
  Computer Science}, pages 276--300, Bad Malente, Germany, September 1997.
  Springer-Verlag.

\bibitem{Kolano99:ARTS}
Paul~Z. Kolano.
\newblock Proof assistance for real-time systems using an interactive theorem
  prover.
\newblock In J.-P. Katoen, editor, {\em Formal Methods for Real-Time and
  Probabilistic Systems (Proceedings 5th International {AMAST} Workshop,
  {ARTS'99})}, volume 1601 of {\em Lecture Notes in Computer Science}, pages
  315--333, Bamberg, Germany, May 1999. Springer-Verlag.

\bibitem{Kolano-etal00:FASE}
Paul Kolano, Richard Kemmerer, and Dino Mandrioli.
\newblock Parallel refinement mechanisms for real-time systems.
\newblock In Tom Maibaum, editor, {\em Fundamental Approaches to Software
  Engineering, {FASE} 2000}, number 1783 in Lecture Notes in Computer Science,
  pages 35--50, Berlin, Germany, March/April 2000. Springer-Verlag.

\bibitem{Muthiayen00}
Darmalingum Muthiayen.
\newblock {\em Real-Time Reactive System Development---A Formal Approach Based
  on {UML} and {PVS}}.
\newblock PhD thesis, Department of Computer Science at Concordia University,
  Montreal, Canada, January 2000.

\bibitem{Shankar93:CAV}
Natarajan Shankar.
\newblock Verification of real-time systems using {PVS}.
\newblock In Costas Courcoubetis, editor, {\em Computer-Aided Verification, CAV
  '93}, volume 697 of {\em Lecture Notes in Computer Science}, pages 280--291,
  Elounda, Greece, June/July 1993. Springer-Verlag.

\bibitem{Skakkebaek94:thesis}
Jens~Ulrik Skakkeb{\ae}k.
\newblock {\em A Verification Assistant for a Real-Time Logic}.
\newblock PhD thesis, Department of Computer Science, Technical University of
  Denmark, Lyngby, Denmark, November 1994.

\bibitem{Skakkebaek&Shankar94}
Jens~U. Skakkeb{\ae}k and N.~Shankar.
\newblock Towards a {Duration Calculus} proof assistant in {PVS}.
\newblock In H.~Langmaack, W.-P. {de Roever}, and J.~Vytopil, editors, {\em
  Formal Techniques in Real-Time and Fault-Tolerant Systems}, volume 863 of
  {\em Lecture Notes in Computer Science}, pages 660--679, L\"{u}beck, Germany,
  September 1994. Springer-Verlag.

\bibitem{Kellomaki97}
Pertti Kellom\"{a}ki.
\newblock Verification of reactive systems using {DisCo} and {PVS}.
\newblock In {\em Formal Methods Europe {FME '97}}, volume 1313 of {\em Lecture
  Notes in Computer Science}, pages 589--604, Graz, Austria, September 1997.
  Springer-Verlag.

\bibitem{AHhart97}
M.~Archer and C.~Heitmeyer.
\newblock Verifying hybrid systems modeled as timed automata: A case study.
\newblock In Oded Maler, editor, {\em Proceedings of the International Workshop
  on Hybrid and Real-Time Systems (HART'97)}, volume 1201 of {\em Lecture Notes
  in Computer Science}, pages 171--185, Grenoble, France, March 1997.
  Springer-Verlag.

\bibitem{Henzinger&Rusu98}
Thomas~A. Henzinger and Vlad Rusu.
\newblock Reachability verification for hybrid automata.
\newblock In Thomas~A. Henzinger and Shankar Sastry, editors, {\em Hybrid
  Systems: Computation and Control (First International Workshop, {HSCC'98})},
  volume 1386 of {\em Lecture Notes in Computer Science}, pages 190--204,
  Berkeley, CA, April 1998. Springer-Verlag.

\bibitem{Hooman96:boiler}
Jan Vitt and Jozef Hooman.
\newblock Assertional specification and verification using {PVS} of the steam
  boiler control system.
\newblock In Jean-Raymond Abrial, Egon Boerger, and Hans Langmaack, editors,
  {\em Formal Methods for Industrial Applications: Specifying and Programming
  the Steam Boiler Control}, volume 1165 of {\em Lecture Notes in Computer
  Science}, pages 453--472. Springer-Verlag, 1996.

\bibitem{Bloo-etal00:SAC}
Roel Bloo, Jozef Hooman, and Edwin de~Jong.
\newblock Semantical aspects of an architecture for distributed embedded
  systems.
\newblock In {\em Proceedings of the 2000 ACM Symposium on Applied Computing
  {(SAC 2000)}}, volume~1, pages 149--155, Como, Italy, March 2000. Association
  for Computing Machinery.

\bibitem{deJong00:ECBS}
Edwin de~Jong, Jaco van~de Pol, and Jozef Hooman.
\newblock Refinement in requirements specification and analysis: A case study.
\newblock In {\em 7th IEEE International Conference and Workshop on the
  Engineering of Computer Based Systems {(ECBS)}}, pages 290--298, Edinburgh,
  Scotland, April 2000. IEEE Computer Society.

\bibitem{vandePol-etal99:IFM}
Jaco van~de Pol, Jozef Hooman, and Edwin de~Jong.
\newblock Modular formal specification of data and behaviour.
\newblock In K.~Araki, A.~Galloway, and K.~Taguchi, editors, {\em Proceedings
  1st Conference on Integrated Formal Methods {(IFM'99)}}, pages 109--128,
  York, UK, June 1999. Springer.

\bibitem{deBoer&Hulst96}
Frank~S. de~Boer and Marten van Hulst.
\newblock Local nondeterminism in asynchronously communicating processes.
\newblock In {\em Formal Methods Europe {FME '96}}, volume 1051 of {\em Lecture
  Notes in Computer Science}, pages 367--384, Oxford, UK, March 1996.
  Springer-Verlag.

\bibitem{Chernyskhovsky:FMPPTA99}
Victoria Chernyakhovsky, Peter Frey, Radharamanan Radhakrihnan, Philip~A.
  Wilsey, Perry Alexander, and Harold~W. Carter.
\newblock A formal framework for specifying and verifying time warp
  optimizations.
\newblock In Jos\'{e} Rolim et~al., editors, {\em Parallel and Distributed
  Processing (Combined Proceedings of 11 Workshops)}, volume 1586 of {\em
  Lecture Notes in Computer Science}, pages 1228--1242, San Juan, Puerto Rico,
  April 1999. Springer-Verlag.
\newblock Presented at the Workshop on Formal Methods for Parallel Programming:
  Theory and Applications {(FMPPTA)}.

\bibitem{Frey99:HICSS}
Peter Frey, Radharamanan Radhakrishnan, Philip~A. Wilsey, Perry Alexander, and
  Harold~W. Carter.
\newblock An extensible formal framework for the specification and verification
  of an optimistic simulation protocol.
\newblock In {\em Proceedings of the 32nd Annual Hawaii International
  Conference on System Sciences}. IEEE Computer Society, January 1999.
\newblock Available at
  \url{http://computer.org/conferen/proceed/hicss/0001/00013/00013049abs.htm}.

\bibitem{Hooman98:TOOLS96}
Jozef Hooman.
\newblock Developing proof rules for distributed real-time systems with {PVS}.
\newblock In Bettina Buth, Rudolf Berghammer, and Jan Peleska, editors, {\em
  Tools for System Development and Verification}, BISS Monographs, pages
  120--139, Aachen, Germany, 1998. Shaker Verlag.
\newblock Proceedings of a workshop held at Bremen in 1996.

\bibitem{Kellomaki95}
Pertti Kellom\"{a}ki.
\newblock Mechanizing invariant proofs of joint action systems.
\newblock In {\em Fourth Symposium on Programming Languages and Software
  Tools}, pages 141--152, Visegrad, Hungary, June 1995.
\newblock Available at
  \url{http://www.cs.tut.fi/~pk/papers/visegrad-95/visegrad.ps.gz}.

\bibitem{Kellomaki96:tphols}
Pertti Kellom\"{a}ki.
\newblock Using auxiliary knowledge in automating invariant proofs.
\newblock In {\em International Conference on Theorem Proving in Higher Order
  Logics}, pages 57--68, Turku, Finland, August 1996.
\newblock Supplementary proceedings, available at
  \url{http://www.tucs.abo.fi/publications/general/G1.html}.

\bibitem{Lesens&Saidi97}
David Lesens and Hassen Sa{\"\i}di.
\newblock Automatic verification of parameterized networks of processes by
  abstraction.
\newblock In Faron Moller, editor, {\em 2nd International Workshop on
  Verification of Infinite State Systems: Infinity '97}, volume~9 of {\em
  Electronic Notes in Theoretical Computer Science}, Bologna, Italy, July 1997.
  Elsevier.
\newblock Available at
  \url{http://www.elsevier.nl/cas/tree/store/tcs/free/entcs/store/tcs9/tcs9009
  .ps}.

\bibitem{Shankar93:lazy}
N.~Shankar.
\newblock A lazy approach to compositional verification.
\newblock Technical Report SRI-CSL-93-8, Computer Science Laboratory, SRI
  International, Menlo Park, CA, December 1993.

\bibitem{vanHulst:thesis}
Marten van Hulst.
\newblock {\em Compositional Verification of Parallel Programs using Epistemic
  Logic and Abstract Assertional Languages}.
\newblock PhD thesis, Faculteit Wiskunde en Informatica, Universiteit Utrecht,
  The Netherlands, June 1995.

\bibitem{Hooman95}
Jozef Hooman.
\newblock Verifying part of the {ACCESS.bus} protocol using {PVS}.
\newblock In P.~S. Thiagarajan, editor, {\em 15th Conference on the Foundations
  of Software Technology and Theoretical Computer Science}, volume 1026 of {\em
  Lecture Notes in Computer Science}, pages 96--110, Bangalore, India, December
  1995. Springer-Verlag.

\bibitem{Havelund&Shankar96}
Klaus Havelund and N.~Shankar.
\newblock Experiments in theorem proving and model checking for protocol
  verification.
\newblock In {\em Formal Methods Europe {FME '96}}, volume 1051 of {\em Lecture
  Notes in Computer Science}, pages 662--681, Oxford, UK, March 1996.
  Springer-Verlag.

\bibitem{Khune-etal97}
Lars Kh\"{u}ne, Jozef Hooman, and Willem-Paul de~Roever.
\newblock Towards mechanical verification of parts of the {IEEE P1394} serial
  bus.
\newblock In {\em 2nd International Workshop on Applied Formal Methods in
  System Design}, Zagreb, Croatia, June 1997.
\newblock Available at \url{http://www.win.tue.nl/cs/tt/hooman/P1394.html}.

\bibitem{Mokkedem&Leonard00:TPHOLS}
Abdel Mokkedem and Tim Leonard.
\newblock Formal verification of the {Alpha} 21364 network protocol.
\newblock In Mark Aargaard and John Harrison, editors, {\em Theorem Proving in
  Higher Order Logics: 13th International Conference, {TPHOLs 2000}}, volume
  1869 of {\em Lecture Notes in Computer Science}, pages 443--461, Portland,
  OR, August 2000. Springer-Verlag.

\bibitem{Rusinowitch-etal00:CAV}
Micha\"{e}l Rusinowitch, Sorin Stratulat, and Francis Klay.
\newblock Mechanical verification of a generic incremental {ABR} conformance
  algorithm.
\newblock In E.~A. Emerson and A.~P. Sistla, editors, {\em Computer-Aided
  Verification, CAV '2000}, volume 1855 of {\em Lecture Notes in Computer
  Science}, pages 344--357, Chicago, IL, July 2000. Springer-Verlag.

\bibitem{Herbert-etal:FM99}
John Herbert, Bruno Dutertre, Robert Riemenschneider, and Victoria Stavridou.
\newblock A formalization of software architecture.
\newblock In Jeannette Wing and Jim Woodcock, editors, {\em FM99: The World
  Congress in Formal Methods}, volume 1708 and 1709 of {\em Lecture Notes in
  Computer Science}, pages 116--133, Toulouse, France, September 1999.
  Springer-Verlag.
\newblock Pages 1--938 are in the first volume, 939--1872 in the second.

\bibitem{Hooman97}
Jozef Hooman.
\newblock Program design in {PVS}.
\newblock In K.Berghammer, J.Peleska, and B.~Buth, editors, {\em Workshop on
  Tool Support for System Development and Verification}, Bremen, Germany, 1997.
\newblock Available at \url{http://www.win.tue.nl/cs/tt/hooman/PDPVS.html}.

\bibitem{Levy&Trilling:FM99}
Michel L\'{e}vy and Laurent Trilling.
\newblock A {PVS}-based approach for teaching constructing correct iterations.
\newblock In Jeannette Wing and Jim Woodcock, editors, {\em FM99: The World
  Congress in Formal Methods}, volume 1708 and 1709 of {\em Lecture Notes in
  Computer Science}, pages 1859--1860, Toulouse, France, September 1999.
  Springer-Verlag.
\newblock Pages 1--938 are in the first volume, 939--1872 in the second.

\bibitem{Verhoeven&Backhouse:FM99}
Richard Verhoeven and Roland Backhouse.
\newblock Interfacing program construction and verification.
\newblock In Jeannette Wing and Jim Woodcock, editors, {\em FM99: The World
  Congress in Formal Methods}, volume 1708 and 1709 of {\em Lecture Notes in
  Computer Science}, pages 1128--1146, Toulouse, France, September 1999.
  Springer-Verlag.
\newblock Pages 1--938 are in the first volume, 939--1872 in the second.

\bibitem{Behnke98:TOOLS96}
Ralf Behnke, Rudolf Berghammer, and S\"{o}nke Magnussen.
\newblock Supporting algebraic program derivation by {PVS}.
\newblock In Bettina Buth, Rudolf Berghammer, and Jan Peleska, editors, {\em
  Tools for System Development and Verification}, BISS Monographs, pages
  22--40, Aachen, Germany, 1998. Shaker Verlag.
\newblock Proceedings of a workshop held at Bremen in 1996.

\bibitem{Dold95}
Axel Dold.
\newblock Representing, verifying and applying software development steps using
  the {PVS} system.
\newblock In V.~S. Alagar and Maurice Nivat, editors, {\em Algebraic
  Methodology and Software Technology, AMAST'95}, volume 936 of {\em Lecture
  Notes in Computer Science}, pages 431--445, Montreal, Canada, July 1995.
  Springer-Verlag.

\bibitem{Dold:PhD}
Axel Dold.
\newblock {\em Formal Software Development using Generic Development Steps}.
\newblock PhD thesis, Universit{\"a}t Ulm, Germany, 2000.

\bibitem{Shankar:MPC95}
N.~Shankar.
\newblock Computer-aided computing.
\newblock In Bernhard M\"oller, editor, {\em Mathematics of Program
  Construction '95}, volume 947 of {\em Lecture Notes in Computer Science},
  pages 50--66. Springer-Verlag, 1995.

\bibitem{Shankar:SCP96}
N.~Shankar.
\newblock Steps towards mechanizing program transformations using {PVS}.
\newblock {\em Science of Computer Programming}, 26(1--3):33--57, 1996.

\bibitem{Jacobs97}
Bart Jacobs.
\newblock Behaviour-refinement of coalgebraic specifications with coinductive
  correctness proofs.
\newblock In Michel Bidoit and Max Dauchet, editors, {\em {TAPSOFT} '97: Theory
  and Practice of Software Development}, volume 1214 of {\em Lecture Notes in
  Computer Science}, pages 787--802, Lille, France, April 1997.
  Springer-Verlag.

\bibitem{Jacobs97:AMAST}
Bart Jacobs.
\newblock Invariants, bisimulations and the correctness of coalgebraic
  refinements.
\newblock In Michael Johnson, editor, {\em Algebraic Methodology and Software
  Technology, {AMAST}'97}, volume 1349 of {\em Lecture Notes in Computer
  Science}, pages 276--291, Sydney, Australia, December 1997. Springer-Verlag.

\bibitem{Jackson00:TPHOLS}
Paul Jackson.
\newblock Total-correctness refinement for sequential reactive systems.
\newblock In Mark Aargaard and John Harrison, editors, {\em Theorem Proving in
  Higher Order Logics: 13th International Conference, {TPHOLs 2000}}, volume
  1869 of {\em Lecture Notes in Computer Science}, pages 320--337, Portland,
  OR, August 2000. Springer-Verlag.

\bibitem{Knappmann96}
Jens Knappmann.
\newblock A {PVS} based tool for developing programs in the {Refinement
  Calculus}.
\newblock Master's thesis, Institut f\"{u}r Informatik und Praktische
  Mathematik der Christian-Albrechts-Universit\"{a}t zu Kiel, Kiel, Germany,
  October 1996.

\bibitem{K-HButh95}
Karl-Heinz Buth.
\newblock Automated code generator verification based on algebraic laws.
\newblock Procos II Report Kiel KHB 5/1, Christian-Albrechts Universit{\"a}t zu
  Kiel, Kiel, Germany, September 1995.
\newblock Available at
  \url{ftp://ftp.informatik.uni-kiel.de/pub/kiel/procos/kiel-khb-5-1.ps.Z}.

\bibitem{Dold-etal97}
A.~Dold, F.~W. von Henke, H.~Pfeifer, and H.~Rue{\ss}.
\newblock Formal verification of transformations for peephole optimiztion.
\newblock In {\em Formal Methods Europe {FME '97}}, volume 1313 of {\em Lecture
  Notes in Computer Science}, pages 459--472, Graz, Austria, September 1997.
  Springer-Verlag.

\bibitem{DGVZ98}
A.~Dold, T.~Gaul, V.~Vialard, and W.~Zimmermann.
\newblock {{ASM}-Based Mechanized Verification of Compiler Backends}.
\newblock In Uwe Gl{\"a}sser and Peter~H. Schmitt, editors, {\em Proceedings of
  the 5th International Workshop on Abstract State Machines}, pages 50--67,
  Magdeburg, Germany, September 1998.
\newblock Available at
  \url{http://i44www.info.uni-karlsruhe.de/~verifix/pres/paper/ASM-WS98-DGVZ.p
  s.gz}.

\bibitem{Dold-etal98:STTT}
Axel Dold, Thilo Gaul, and Wolf Zimmermann.
\newblock Mechanized verification of compiler backends.
\newblock In Tiziana Margaria and Bernhard Steffen, editors, {\em Proceedings
  of the International Workshop on Software Tools for Technology Transfer
  {STTT'98}}, pages 13--22, Aalborg, Denmark, June 1998. BRICS NS-98-4.
\newblock Proceedings available at \url{http://www.brics.dk/NS/98/4/}.

\bibitem{Dold&Vialard99}
Axel Dold and Vincent Vialard.
\newblock Formal verification of a compiler back-end generic checker program.
\newblock In D.~Bj{\o}rner, M.~Broy, and A.V. Zamulin, editors, {\em Third
  International {Andrei Ershov} Memorial Conference: Perspectives of System
  Informatics, {PSI'99}}, volume 1755 of {\em Lecture Notes in Computer
  Science}, pages 470--480, Novosibirsk, Russia, July 1999. Springer-Verlag.

\bibitem{Stringer-Calvert97}
David W.~J. Stringer-Calvert, Susan Stepney, and Ian Wand.
\newblock Using {PVS} to prove a {Z} refinement: A case study.
\newblock In {\em Formal Methods Europe {FME '97}}, volume 1313 of {\em Lecture
  Notes in Computer Science}, pages 573--588, Graz, Austria, September 1997.
  Springer-Verlag.

\bibitem{Stringer-Calvert98:thesis}
David W.~J. Stringer-Calvert.
\newblock {\em Mechanical Verification of Compiler Correctness}.
\newblock PhD thesis, University of York, Department of Computer Science, York,
  England, March 1998.
\newblock Available at
  \url{http://www.csl.sri.com/~dave_sc/papers/thesis.html}.

\bibitem{Wahab:UWARWICK:CS-RR-354}
M.~Wahab.
\newblock Verification and abstraction of flow-graph programs with pointers and
  computed jumps.
\newblock Research Report CS-RR-354, Department of Computer Science, University
  of Warwick, Coventry, UK, November 1998.
\newblock Available at
  \url{http://www.dcs.warwick.ac.uk/pub/reports/rr/354.html}.

\bibitem{Wahab98}
Matthew Wahab.
\newblock {\em Object Code Verification}.
\newblock PhD thesis, Department of Computer Science, University of Warwick,
  Coventry, UK, December 1998.
\newblock Available at
  \url{http://www.dcs.warwick.ac.uk/pub/reports/theses/wahab98.html}.

\bibitem{Arons99:VLSI}
Tamara Arons and Amir Pnueli.
\newblock Verifying {Tomasulo'}s algorithm by refinement.
\newblock In {\em The Twelfth International Conference on {VLSI} Design}, pages
  306--309, Goa, India, January 1999. IEEE Computer Society.

\bibitem{Arons&Pnueli00:TACAS}
Tamarah Arons and Amir Pnueli.
\newblock A comparison of two verification methods for speculative instruction
  execution.
\newblock In Susanne Graf and Michael Schwartzbach, editors, {\em Tools and
  Algorithms for the Construction and Analysis of Systems {(TACAS 2000)}},
  number 1785 in Lecture Notes in Computer Science, pages 487--502, Berlin,
  Germany, March 2000. Springer-Verlag.

\bibitem{Cyrluk96:FMCAD}
David Cyrluk.
\newblock Inverting the abstraction mapping: A methodology for hardware
  verification.
\newblock In Mandayam Srivas and Albert Camilleri, editors, {\em Formal Methods
  in Computer-Aided Design (FMCAD '96)}, volume 1166 of {\em Lecture Notes in
  Computer Science}, pages 172--186, Palo Alto, CA, November 1996.
  Springer-Verlag.

\bibitem{Cyrluk97:ICFEM}
David Cyrluk, John Rushby, and Mandayam Srivas.
\newblock Systematic formal verification of interpreters.
\newblock In Michael~G. Hinchey and Shaoying Liu, editors, {\em First
  International Conference on Formal Engineering Methods (ICFEM '97)}, pages
  140--149, Hiroshima, Japan, November 1997. IEEE Computer Society.

\bibitem{Damm&Pnueli97}
Werner Damm and Amir Pnueli.
\newblock Verifying out-of-order executions.
\newblock In Hon~F. li and David~K. Probst, editors, {\em Advances in Hardware
  Design and Verification: {IFIP WG10.5} International Conference on Correct
  Hardware Design and Verification Methods (CHARME)}, pages 23--47, Montreal,
  Canada, October 1997. Chapman \& Hall.

\bibitem{Fisler94:TPCD}
Kathi Fisler.
\newblock Extending formal reasoning with support for hardware diagrams.
\newblock In Ramayya Kumar and Thomas Kropf, editors, {\em Theorem Provers in
  Circuit Design ({TPCD} '94)}, volume 910 of {\em Lecture Notes in Computer
  Science}, pages 298--303, Bad Herrenalb, Germany, September 1994.
  Springer-Verlag.

\bibitem{Gopalakrishnan-etal97}
Ganesh Gopalakrishnan, Rajnish Ghughal, Ravi Hosabettu, Abdelillah Mokkedem,
  and Ratan Nalumasu.
\newblock Formal modeling and validation applied to a commercial coherent bus:
  A case study.
\newblock In Hon~F. li and David~K. Probst, editors, {\em Advances in Hardware
  Design and Verification: {IFIP WG10.5} International Conference on Correct
  Hardware Design and Verification Methods (CHARME)}, pages 48--62, Montreal,
  Canada, October 1997. Chapman \& Hall.

\bibitem{Greve98:FMCAD}
David Greve.
\newblock Symbolic simulation of the {JEM1} microprocessor.
\newblock In Ganesh Gopalakrishnan and Phillip Windley, editors, {\em Formal
  Methods in Computer-Aided Design (FMCAD '98)}, volume 1522 of {\em Lecture
  Notes in Computer Science}, pages 321--333, Palo Alto, CA, November 1998.
  Springer-Verlag.

\bibitem{Hardin98:CAV}
David Hardin, Matthew Wilding, and David Greve.
\newblock Transforming the theorem prover into a digital design tool: From
  concept car to off-road vehicle.
\newblock In Alan~J. Hu and Moshe~Y. Vardi, editors, {\em Computer-Aided
  Verification, CAV '98}, volume 1427 of {\em Lecture Notes in Computer
  Science}, pages 39--44, Vancouver, Canada, June 1998. Springer-Verlag.

\bibitem{Hosabettu98:CAV}
Ravi Hosabettu, Mandayam Srivas, and Ganesh Gopalakrishnan.
\newblock Decomposing the proof of correctness of pipelined microprocessors.
\newblock In Alan~J. Hu and Moshe~Y. Vardi, editors, {\em Computer-Aided
  Verification, CAV '98}, volume 1427 of {\em Lecture Notes in Computer
  Science}, pages 122--134, Vancouver, Canada, June 1998. Springer-Verlag.

\bibitem{Hosabettu:CAV99}
Ravi Hosabettu, Mandayam Srivas, and Ganesh Gopalakrishnan.
\newblock Proof of correctness of a processor with reorder buffer using the
  completion functions approach.
\newblock In Nicolas Halbwachs and Doron Peled, editors, {\em Computer-Aided
  Verification, CAV '99}, volume 1633 of {\em Lecture Notes in Computer
  Science}, pages 47--59, Trento, Italy, July 1999. Springer-Verlag.

\bibitem{Hosabettu:CHARME99}
Ravi Hosabettu, Ganesh Gopalakrishnan, and Mandayam Srivas.
\newblock Proof of correctness of a processor implementing {Tomasulo's}
  algorithm without a reorder buffer.
\newblock In {\em Advances in Hardware Design and Verification: {IFIP WG10.5}
  International Conference on Correct Hardware Design and Verification Methods
  (CHARME '99)}, volume 1703 of {\em Lecture Notes in Computer Science}, pages
  8--22, Bad Herrenalb, Germany, September 1999. Springer-Verlag.

\bibitem{Hosabettu-etal00:CAV}
Ravi Hosabettu, Ganesh Gopalakrishnan, and Mandayam Srivas.
\newblock Verifying microarchitectures that support speculation and exceptions.
\newblock In E.~A. Emerson and A.~P. Sistla, editors, {\em Computer-Aided
  Verification, CAV '2000}, volume 1855 of {\em Lecture Notes in Computer
  Science}, pages 521--537, Chicago, IL, July 2000. Springer-Verlag.

\bibitem{Johnson94:TPCD}
Steven~D. Johnson, Paul~S. Miner, and Albert Camlleri.
\newblock Studies of the single-pulser in various reasoning systems.
\newblock In Ramayya Kumar and Thomas Kropf, editors, {\em Theorem Provers in
  Circuit Design ({TPCD} '94)}, volume 910 of {\em Lecture Notes in Computer
  Science}, pages 126--145, Bad Herrenalb, Germany, September 1994.
  Springer-Verlag.

\bibitem{Johnson&Miner97}
Steven~D. Johnson and Paul~S. Miner.
\newblock Integrated reasoning support in system design: Design derivation and
  theorem proving.
\newblock In Hon~F. li and David~K. Probst, editors, {\em Advances in Hardware
  Design and Verification: {IFIP WG10.5} International Conference on Correct
  Hardware Design and Verification Methods (CHARME)}, pages 255--272, Montreal,
  Canada, October 1997. Chapman \& Hall.

\bibitem{Leathrum97:LFM}
James {Leathrum, Jr.}
\newblock Fundamental hardware design in {PVS}.
\newblock In C.~Michael Holloway and Kelly~J. Hayhurst, editors, {\em LFM' 97:
  Fourth NASA Langley Formal Methods Workshop}, NASA Conference Publication
  3356, pages 193--204, Hampton, VA, September 1997. NASA Langley Research
  Center.
\newblock Available at \url{http://atb-www.larc.nasa.gov/Lfm97/proceedings/}.

\bibitem{Li-etal97}
Xiaoshan Li, Antonio Cau, Ben Moszkowski, Nick Coleman, and Hussein Zedan.
\newblock Proving the correctness of the interlock mechanism in processor
  design.
\newblock In Hon~F. li and David~K. Probst, editors, {\em Advances in Hardware
  Design and Verification: {IFIP WG10.5} International Conference on Correct
  Hardware Design and Verification Methods (CHARME)}, pages 5--22, Montreal,
  Canada, October 1997. Chapman \& Hall.

\bibitem{Miner&Johnson96}
Paul~S. Miner and Steven~D. Johnson.
\newblock Verification of an optimized fault-tolerant clock synchronization
  circuit: A case study exploring the boundary between formal reasoning
  systems.
\newblock In Mary Sheeran and Satnam Singh, editors, {\em Designing Correct
  Circuits}, Bastad, Sweden, September 1996. Electronic Workshops in Computing
  (\url{http://ewic.org.uk/ewic/}).

\bibitem{Miner94:circuit}
Paul~S. Miner, Shyamsundar Pullela, and Steven~D. Johnson.
\newblock Interaction of formal design systems in the development of a
  fault-tolerant clock synchronization circuit.
\newblock In {\em 13th Symposium on Reliable Distributed Systems}, pages
  128--137, Dana Point, CA, October 1994. IEEE Computer Society.

\bibitem{Miner96:FMCAD}
Paul~S. Miner and James~F. {Leathrum, Jr.}
\newblock Verification of {IEEE} compliant subtractive division algorithms.
\newblock In Mandayam Srivas and Albert Camilleri, editors, {\em Formal Methods
  in Computer-Aided Design (FMCAD '96)}, volume 1166 of {\em Lecture Notes in
  Computer Science}, pages 64--78, Palo Alto, CA, November 1996.
  Springer-Verlag.

\bibitem{Miller&Srivas95}
Steven~P. Miller and Mandayam Srivas.
\newblock Formal verification of the {AAMP5} microprocessor: A case study in
  the industrial use of formal methods.
\newblock In {\em WIFT '95: Workshop on Industrial-Strength Formal
  Specification Techniques}, pages 2--16, Boca Raton, FL, 1995. IEEE Computer
  Society.

\bibitem{Pnueli98:FMCAD}
Amir Pnueli and Tamara Arons.
\newblock Verification of data-insensitive circuits: An in-order-retirement
  case study.
\newblock In Ganesh Gopalakrishnan and Phillip Windley, editors, {\em Formal
  Methods in Computer-Aided Design (FMCAD '98)}, volume 1522 of {\em Lecture
  Notes in Computer Science}, pages 351--368, Palo Alto, CA, November 1998.
  Springer-Verlag.

\bibitem{Ruess96:CAV}
H.~Rue{\ss}, N.~Shankar, and M.~K. Srivas.
\newblock Modular verification of {SRT} division.
\newblock In Rajeev Alur and Thomas~A. Henzinger, editors, {\em Computer-Aided
  Verification, CAV '96}, volume 1102 of {\em Lecture Notes in Computer
  Science}, pages 123--134, New Brunswick, NJ, July/August 1996.
  Springer-Verlag.

\bibitem{Ruess99:FMSD}
H.~Rue{\ss}, N.~Shankar, and M.~K. Srivas.
\newblock Modular verification of {SRT} division.
\newblock {\em Formal Methods in Systems Design}, 14(1):45--73, January 1999.

\bibitem{Sree97:AMAST}
Sreeranga~P. Rajan and Masahiro Fujita.
\newblock {ATM} switch design: Parametric high-level modeling and formal
  verification.
\newblock In Michael Johnson, editor, {\em Algebraic Methodology and Software
  Technology, {AMAST}'97}, volume 1349 of {\em Lecture Notes in Computer
  Science}, pages 437--450, Sydney, Australia, December 1997. Springer-Verlag.

\bibitem{Sree98:todaes}
S.~P. Rajan, M.~Fujita, K.~Yuan, and M.~T-C. Lee.
\newblock {ATM} switch design by high level modeling, formal verification, and
  high level synthesis.
\newblock {\em ACM Transactions on Design Automation of Electronic Systems
  (TODAES)}, 3(4):554--562, October 1998.

\bibitem{Srivas&Miller95:chdl}
Mandayam~K. Srivas and Steven~P. Miller.
\newblock Applying formal verification to a commercial microprocessor.
\newblock In Steven~D. Johnson, editor, {\em {CHDL '95}: 12th Conference on
  Computer Hardware Description Languages and their Applications}, pages
  493--502, Chiba, Japan, August 1995. Proceedings published in a single volume
  jointly with ASP-DAC '95, CHDL '95, and VLSI '95, IEEE Catalog no.\ 95TH8102.

\bibitem{Srivas&Miller95:inbook}
Mandayam~K. Srivas and Steven~P. Miller.
\newblock Formal verification of the {AAMP5} microprocessor.
\newblock In Michael~G. Hinchey and Jonathan~P. Bowen, editors, {\em
  Applications of Formal Methods}, Prentice Hall International Series in
  Computer Science, chapter~7, pages 125--180. Prentice Hall, Hemel Hempstead,
  UK, 1995.

\bibitem{Srivas&Miller96:FMSD}
Mandayam~K. Srivas and Steven~P. Miller.
\newblock Applying formal verification to the {AAMP5} microprocessor: A case
  study in the industrial use of formal methods.
\newblock {\em Formal Methods in Systems Design}, 8(2):153--188, March 1996.

\bibitem{Mansouri00:FMSD}
Nazanin Mansouri and Ranga Vemuri.
\newblock Automated correctness condition generation for formal verification of
  synthesized {RTL} designs.
\newblock {\em Formal Methods in Systems Design}, 16(1):59--91, January 2000.

\bibitem{Naren98:ICCD}
Naren Narasimhan, Elena Teica, Rajesh Radhakrishnan, Sriram Govindarajan, and
  Ranga Vemuri.
\newblock Theorem proving guided development of formal assertions in a
  resource-constrained scheduler for high-level synthesis.
\newblock In Andreas Kuehlmann, editor, {\em International Conference on
  Computer Design ({ICCD}'98)}, Austin, TX, October 1998. IEEE Computer
  Society.

\bibitem{Naren98:tphols}
Naren Narasimhan and Ranga Vemuri.
\newblock On the effectiveness of theorem proving guided discovery of formal
  assertions for a register allocator in a high-level synthesis system.
\newblock In Jim Grundy and Malcolm Newey, editors, {\em Theorem Proving in
  Higher Order Logics: 11th International Conference, {TPHOLs '98}}, volume
  1479 of {\em Lecture Notes in Computer Science}, pages 367--386, Canberra,
  Australia, September 1998. Springer-Verlag.

\bibitem{Sree94:Philips}
P.~Sreeranga Rajan.
\newblock Transformations in high level synthesis: Specification and
  verification.
\newblock Technical Report NL-TN 118/94, Philips Research Laboratories,
  Eindhoven, The Netherlands, April 1994.
\newblock Revised version available as SRI Technical Report SRI-CSL-94-10,
  October 1994.

\bibitem{Sree95:chdl}
Sreeranga~P. Rajan.
\newblock Correctness of transformations in high level synthesis.
\newblock In Steven~D. Johnson, editor, {\em {CHDL '95}: 12th Conference on
  Computer Hardware Description Languages and their Applications}, pages
  597--603, Chiba, Japan, August 1995. Proceedings published in a single volume
  jointly with ASP-DAC '95, CHDL '95, and VLSI '95, IEEE Catalog no.\ 95TH8102.

\bibitem{Sree:thesis}
Sreeranga~P. Rajan.
\newblock {\em Transformations on Dependency Graphs: Formal Specification and
  Efficient Mechanical Verification}.
\newblock PhD thesis, Department of Computer Science, University of British
  Columbia, Vancouver, Canada, October 1995.

\bibitem{Nalumasu&Ganesh98}
Ratan Nalumasu and Ganesh Gopalakrishnan.
\newblock Deriving efficient cache coherence protocols through refinement.
\newblock In {\em Formal Methods for Parallel Programming: Theory and
  Applications {(FMPPTA)}}, Orlando, FL, March 98.
\newblock Available at \url{http://www.loria.fr/~mery/lncs_fmppta98/paper7.ps}.

\bibitem{Park:thesis}
Seungjoon Park.
\newblock {\em Computer Assisted Analysis of Multiprocessor Memory Systems}.
\newblock PhD thesis, Department of Electrical Engineering, Stanford
  University, June 1996.

\bibitem{Park&Dill96:PDS}
Seungjoon Park and David~L. Dill.
\newblock An executable specification, analyzer and verifier for relaxed memory
  order: With formal proofs.
\newblock Submitted for publication; an earlier version (without proofs) is
  available~\cite{Park&Dill95:spaa}, 1996.

\bibitem{Park&Dill98:TCS}
Seungjoon Park and David~L. Dill.
\newblock Verification of cache coherence protocols by aggregation of
  distributed transactions.
\newblock {\em Theory of Computing Systems}, 31(4):355--376, 1998.

\bibitem{Rajan95:multimedia}
Sreeranga Rajan, P.~Venkat Rangan, and Harrick~M. Vin.
\newblock A formal basis for structured multimedia collaborations.
\newblock In {\em Proceedings of the 2nd IEEE International Conference on
  Multimedia Computing and Systems}, pages 194--201, Washington, DC, May 1995.
  IEEE Computer Society.

\bibitem{rbj00}
V.~Rusu, L.~du~Bousquet, and T.~J\'{e}ron.
\newblock An approach to symbolic test generation.
\newblock In {\em 2nd International Workshop on Integrated Formal Method
  (IFM'00)}, number 1945 in Lecture Notes in Computer Science, pages 338--357,
  Dagstuhl, Germany, November 2000. Springer-Verlag.

\bibitem{Graham96}
T.~C.~Nicholas Graham.
\newblock A method for the formal testing of program visualization tools.
\newblock In {\em Proceedings of the Fourth Workshop on Program Comprehension},
  pages 45--54, Berlin, Germany, March 1996. IEEE Computer Society.

\bibitem{Suri&Sinha98}
Neeraj Suri and Purnendu Sinha.
\newblock On the use of formal methods for validation.
\newblock In {\em Fault Tolerant Computing Symposium 28}, pages 390--399,
  Munich, Germany, June 1998. IEEE Computer Society.

\bibitem{Sinha&Suri99:FTCS}
Purnendu Sinha and Neeraj Suri.
\newblock Identification of test cases using a formal fault injection approach.
\newblock In {\em Fault Tolerant Computing Symposium 29}, pages 314--321,
  Madison, WI, June 1999. IEEE Computer Society.

\bibitem{Sinha&Suri99:RTSS}
Purnendu Sinha and Neeraj Suri.
\newblock Formal techniques for dependable real time protocols.
\newblock In {\em Real Time Systems Symposium}, Phoenix, AZ, December 1999.
  IEEE Computer Society.

\bibitem{Qadeer&Shankar98}
Shaz Qadeer and Natarajan Shankar.
\newblock Verifying a self-stabilizing mutual exclusion algorithm.
\newblock In David Gries and Willem-Paul de~Roever, editors, {\em IFIP
  International Conference on Programming Concepts and Methods (PROCOMET '98)},
  pages 424--443, Shelter Island, NY, June 1998. Chapman \& Hall.

\bibitem{Kulkarni99:SSS}
Sandeep Kulkarni, John Rushby, and N.~Shankar.
\newblock A case study in component-based mechanical verification of
  fault-tolerant programs.
\newblock In {\em {ICDCS} Workshop on Self-Stabilizing Systems}, pages 33--40,
  Austin, TX, June 1999. IEEE Computer Society.

\bibitem{Gargantini&Riccobene00:ASM}
Angelo Gargantini and Elvinia Riccobene.
\newblock Encoding {Abstract State Machines} in {PVS}.
\newblock In Yuri Gurevich, Phillip~W. Kutter, Martin Odersky, and Lothar
  Thiele, editors, {\em Abstract State Machines: Theory and Applications ({ASM}
  2000)}, number 1912 in Lecture Notes in Computer Science, pages 303--322,
  Monte Verit\`{a}, Switzerland, March 2000. Springer-Verlag.

\bibitem{Bodeveix-etal99}
Jean~Paul Bodeveix, Mamoun Filali, and C\'{e}sar~A. Mu{\~{n}}oz.
\newblock A formalization of the {B-Method} in {Coq} and {PVS}.
\newblock In {\em FM99: The World Congress in Formal Methods, User Group
  Meeting 2. The B-Method: Applying B in an Industrial Context: Tools, Lessons
  and Techniques}, September 1999.
\newblock Available on the CD-ROM for \cite{FM99}.

\bibitem{Munoz&Rushby:FM99}
C\'{e}sar Mu{\~{n}}oz and John Rushby.
\newblock Structural embeddings: Mechanization with method.
\newblock In Jeannette Wing and Jim Woodcock, editors, {\em FM99: The World
  Congress in Formal Methods}, volume 1708 and 1709 of {\em Lecture Notes in
  Computer Science}, pages 452--471, Toulouse, France, September 1999.
  Springer-Verlag.
\newblock Pages 1--938 are in the first volume, 939--1872 in the second.

\bibitem{Paige&Ostroff:FM99}
Richard~F. Paige and Jonathan~S. Ostroff.
\newblock Developing {BON} as an industrial-strength formal method.
\newblock In Jeannette Wing and Jim Woodcock, editors, {\em FM99: The World
  Congress in Formal Methods}, volume 1708 and 1709 of {\em Lecture Notes in
  Computer Science}, pages 834--853, Toulouse, France, September 1999.
  Springer-Verlag.
\newblock Pages 1--938 are in the first volume, 939--1872 in the second.

\bibitem{Bensalem99:DCCA}
S.~Bensalem, P.~Caspi, C.~Parent-Vigouroux, and C.~Dumas.
\newblock A methodology for proving control systems with {Lustre} and {PVS}.
\newblock In Charles~B. Weinstock and John Rushby, editors, {\em Dependable
  Computing for Critical Applications---7}, volume~12 of {\em Dependable
  Computing and Fault Tolerant Systems}, pages 89--107, San Jose, CA, January
  1999. IEEE Computer Society.

\bibitem{Rushby&Srivas:HOL93}
John Rushby and Mandayam Srivas.
\newblock Using {PVS} to prove some theorems of {David Parnas}.
\newblock In Jeffrey~J. Joyce and Carl-Johan~H. Seger, editors, {\em Higher
  Order Logic Theorem Proving and its Applications (6th International Workshop,
  HUG '93)}, volume 780 of {\em Lecture Notes in Computer Science}, pages
  163--173, Vancouver, Canada, August 1993. Springer-Verlag.

\bibitem{Heimdahl&Czerny96}
Mats P.~E. Heimdahl and Barbara~J. Czerny.
\newblock Using {PVS} to analyze hierarchical state-based requirements for
  completeness and consistency.
\newblock In {\em IEEE High-Assurance Systems Engineering Workshop (HASE '96)},
  pages 252--262, Niagara on the Lake, Canada, October 1996.

\bibitem{Heimdahl97:LFM}
Mats~P.E. Heimdahl.
\newblock Verifying communication related safety constraints in {RSML}
  specifications.
\newblock In C.~Michael Holloway and Kelly~J. Hayhurst, editors, {\em LFM' 97:
  Fourth NASA Langley Formal Methods Workshop}, NASA Conference Publication
  3356, pages 115--128, Hampton, VA, September 1997. NASA Langley Research
  Center.
\newblock Available at \url{http://atb-www.larc.nasa.gov/Lfm97/proceedings/}.

\bibitem{Heimdahl97:ICFEM}
Mats P.~E. Heimdahl and Jeffrey~M. Thompson.
\newblock Specification and analysis of system level inter-component
  communication.
\newblock In Michael~G. Hinchey and Shaoying Liu, editors, {\em First
  International Conference on Formal Engineering Methods (ICFEM '97)}, pages
  192--201, Hiroshima, Japan, November 1997. IEEE Computer Society.

\bibitem{Czerny&Heimdahl:ASE98}
Barbara~J. Czerny and Mats P.~E. Heimdahl.
\newblock Automated integrative analysis of state-based requirements.
\newblock In D.~Redmiles and B.~Nuseibeh, editors, {\em Thirteenth IEEE
  Conference on Automated Software Engineering ({ASE '98})}, Nonolulu, Hawaii,
  October 1998. IEEE Computer Society.

\bibitem{Heimdahl98:computer}
Mats P.~E. Heimdahl, Jeffrey~M. Thompson, and Barbara~J. Czerny.
\newblock Specification and analysis of intercomponent communication.
\newblock {\em IEEE Computer}, 31(4):47--54, April 1998.

\bibitem{Agerholm96}
Sten Agerholm.
\newblock Translating specifications in {VDM-SL} to {PVS}.
\newblock In Joakim von Wright, Jim Grundy, and John Harrison, editors, {\em
  Theorem Proving in Higher Order Logics: 9th International Conference, {TPHOLs
  '96}}, volume 1125 of {\em Lecture Notes in Computer Science}, pages 1--16,
  Turku, Finland, August 1996. Springer-Verlag.

\bibitem{Agerholm97:VDMbook}
Sten Agerholm, Juan Bicarregui, and Savi Maharaj.
\newblock On the verification of {VDM} specification and refinement with {PVS}.
\newblock In Juan Bicarregui, editor, {\em Proof in {VDM}: Case Studies}, FACIT
  (Formal Approaches to Computing and Information Technology), chapter~6, pages
  157--190. Springer-Verlag, London, UK, 1997.

\bibitem{Maharaj97:ASE}
Savi Maharaj and Juan Bicarregui.
\newblock On the verification of {VDM} specification and refinement with {PVS}.
\newblock In M.~Lowry and Y.~Ledru, editors, {\em 12th IEEE International
  Conference on Automated Software Engineering ({ASE '97})}, pages 280--289,
  Incline Village, NV, November 1997. IEEE Computer Society.

\bibitem{Alexander-etal:FM99}
Perry Alexander, Murali Rangarajan, and Phillip Baraona.
\newblock A brief summary of {VSPEC}.
\newblock In Jeannette Wing and Jim Woodcock, editors, {\em FM99: The World
  Congress in Formal Methods}, volume 1708 and 1709 of {\em Lecture Notes in
  Computer Science}, pages 1068--1086, Toulouse, France, September 1999.
  Springer-Verlag.
\newblock Pages 1--938 are in the first volume, 939--1872 in the second.

\bibitem{Adams-etal:CADE99}
A.~A. Adams, H.~Gottliebsen, S.~A. Linton, and U.~Martin.
\newblock {VSDITLU}: A verifiable symbolic definite integral table look-up.
\newblock In {\em Automated Deduction---{CADE-16}}, volume 1632 of {\em Lecture
  Notes in Artificial Intelligence}, pages 112--126, Trento, Italy, July 1999.
  Springer-Verlag.

\bibitem{Adams-etal:ISSAC99}
A.~A. Adams, H.~Gottliebsen, S.~A. Linton, and U.~Martin.
\newblock Automated theorem proving in support of computer algebra: Symbolic
  definite integration as a case study.
\newblock In {\em Proceedings of the 1999 International Symposium on Symbolic
  and Algebraic Computation, ({ISSAC '99})}, pages 253--260, Vancouver, B.C.,
  Canada, July 1999. Association for Computing Machinery.

\bibitem{Buth98:TOOLS96}
Bettina Buth, Rachel Cardell-Oliver, and Jan Peleska.
\newblock Combining tools for the verification of fault-tolerant systems.
\newblock In Bettina Buth, Rudolf Berghammer, and Jan Peleska, editors, {\em
  Tools for System Development and Verification}, BISS Monographs, pages
  41--69, Aachen, Germany, 1998. Shaker Verlag.
\newblock Proceedings of a workshop held at Bremen in 1996.

\bibitem{Buth98:tools}
Bettina Buth.
\newblock {PAMELA} + {PVS}.
\newblock In Rudolph Berghammer and Yassine Lakhnech, editors, {\em Tool
  Support for System Specification, Development, and Verification}, Advances in
  Computing Science, pages 62--76, Malente, Germany, June 1998.
  Springer-Verlag.
\newblock Proceedings published in May 1999.

\bibitem{Buth97:AMAST}
Bettina Buth.
\newblock {PAMELA $+$ PVS}.
\newblock In Michael Johnson, editor, {\em Algebraic Methodology and Software
  Technology, {AMAST}'97}, volume 1349 of {\em Lecture Notes in Computer
  Science}, pages 560--562, Sydney, Australia, December 1997. Springer-Verlag.

\bibitem{Corbett-etal00:ICSE}
James Corbett, Matthew Dwyer, John Hatcliff, Corina Pasareanu, Robby, Shawn
  Laubach, and Hongjun Zheng.
\newblock Bandera: Extracting finite-state models from {Java} source code.
\newblock In {\em 22nd International Conference on Software Engineering}, pages
  439--448, Limerick, Ireland, June 2000. IEEE Computer Society.

\bibitem{Compass89}
IEEE Washington Section.
\newblock {\em COMPASS '89 (Proceedings of the Fourth Annual Conference on
  Computer Assurance)}, Gaithersburg, MD, June 1989.

\bibitem{FTCS-highlights}
IEEE Computer Society.
\newblock {\em Fault Tolerant Computing Symposium 25: Highlights from 25
  Years}, Pasadena, CA, June 1995. IEEE Computer Society.

\bibitem{Saiedian96}
Hossein {Saiedian (Ed.)}.
\newblock An invitation to formal methods.
\newblock {\em IEEE Computer}, 29(4):16--30, April 1996.
\newblock A ``roundtable'' of short articles by several authors.

\bibitem{Encress95}
Roger Shaw, editor.
\newblock {\em Safety and Reliability of Software Based Systems (Twelfth Annual
  {CSR} Workshop)}, Bruges, Belgium, September 1995. Springer.

\bibitem{Park&Dill95:spaa}
Seungjoon Park and David~L. Dill.
\newblock An executable specification, analyzer and verifier for {RMO (Relaxed
  Memory Order)}.
\newblock In {\em 7th ACM Symposium on Parallel Algorithms and Architectures},
  pages 34--51, July 1995.

\bibitem{FM99}
Jeannette Wing and Jim Woodcock, editors.
\newblock {\em FM99: The World Congress in Formal Methods}, volume 1708 and
  1709 of {\em Lecture Notes in Computer Science}, Toulouse, France, September
  1999. Springer-Verlag.
\newblock Pages 1--938 are in the first volume, 939--1872 in the second.

\end{thebibliography}

\end{document}
% End of pvs-bib.tex -----------------------------------