\begin{thebibliography}{10}

\bibitem{Clarke:TOPLAS94}
E.M. Clarke, O.~Grumberg, and D.E. Long.
\newblock Model checking and abstraction.
\newblock {\em ACM Transactions on Programming Languages and Systems},
  16(5):1512--1542, September 1994.

\bibitem{Corbett:ICSE00}
James~C. Corbett, Matthew~B. Dwyer, John Hatcliff, Shawn Laubach, Corina~S.
  P\u{a}s\u{a}reanu, Robby, and Hongjun Zheng.
\newblock Bandera : Extracting finite-state models from {Java} source code.
\newblock In {\em Proceedings of the 22nd International Conference on Software
  Engineering}, June 2000.

\bibitem{Dwyer:FMSP98}
Matthew~B. Dwyer, George~S. Avrunin, and James~C. Corbett.
\newblock Property specification patterns for finite-state verification.
\newblock In Mark Ardis, editor, {\em Proceedings of the Second Workshop on
  Formal Methods in Software Practice}, pages 7--15, March 1998.

\bibitem{Dwyer:GPS98}
Matthew~B. Dwyer and Corina~S. Pasareanu.
\newblock Model checking generic container implementations.
\newblock In {\em Proceedings of the 1st Symposium on Generic Programming}, May
  1998.

\bibitem{Dwyer:TR98-12}
Matthew~B. Dwyer, Corina~S. Pasareanu, and James~C. Corbett.
\newblock Translating {A}da programs for model checking : A tutorial.
\newblock Technical Report 98-12, Kansas State University, Department of
  Computing and Information Sciences, 1998.

\bibitem{Dwyer:patterns-web-site}
M.B. Dwyer, G.S. Avrunin, and J.C. Corbett.
\newblock {A System of Specification Patterns}.
\newblock \url|http://www.cis.ksu.edu/santos/spec-patterns|, 1998.

\bibitem{Dwyer:ICSE99}
M.B. Dwyer, G.S. Avrunin, and J.C. Corbett.
\newblock Patterns in property specifications for finite-state verification.
\newblock In {\em Proceedings of the 21st International Conference on Software
  Engineering}, May 1999.

\bibitem{Grove:PhD}
David~Paul Grove.
\newblock {\em Effective Interprocedural Optimization of Object-oriented
  Languages}.
\newblock PhD thesis, University of Washington, 1998.

\bibitem{Hatcliff:SAS99}
John Hatcliff, James~C. Corbett, Matthew~B. Dwyer, Stefan Sokolowski, and
  Hongjun Zheng.
\newblock A formal study of slicing for multi-threaded programs with {JVM}
  concurrency primitives.
\newblock In {\em Proceedings of the 6th International Static Analysis
  Symposium (SAS'99)}, September 1999.

\bibitem{Hatcliff:HOSC00}
John Hatcliff, Matthew~B. Dwyer, and Hongjun Zheng.
\newblock Slicing software for model construction.
\newblock {\em Higher-order and Symbolic Computation}, 2000.
\newblock to appear.

\bibitem{Huth-Ryan:99}
M.~Huth and M.~Ryan.
\newblock {\em Logic in {C}omputer {S}cience: {M}odelling and {R}easoning about
  {S}ystems}.
\newblock Cambridge University Press, 1999.
\newblock To appear.

\bibitem{Kramer:TOOLS98}
Reto Kramer.
\newblock {iContract}---the {J}ava {D}esign by {C}ontract tool.
\newblock In {\em Proceedings of Technology of Object-Oriented Languages and
  Systems, TOOLS-USA}. IEEE Press, 1998.

\bibitem{Manna:BOOK91}
Z.~Manna and A.~Pnueli.
\newblock {\em The Temporal Logic of Reactive and Concurrent Systems:
  Specification}.
\newblock Springer-Verlag, 1991.

\bibitem{Penix:ICSE00}
John Penix, Willem Visser, Eric Engstrom, Aaron Larson, and Nichloas Weininger.
\newblock Verification of time partitioning in the deos scheduler kernel.
\newblock In {\em Proceedings of the 22nd International Conference on Software
  Engineering}, June 2000.

\bibitem{Valle-Rai:CASCON99}
Raja Valle-Rai, Laurie Hendren, Vijay Sundaresan, Patrick Lam, Etienne Gagnon,
  and Phong Co.
\newblock Soot - a {J}ava optimization framework.
\newblock In {\em Proceedings of CASCON'99}, November 1999.

\end{thebibliography}
