\begin{thebibliography}{10}
\expandafter\ifx\csname url\endcsname\relax
  \def\url#1{\texttt{#1}}\fi
\expandafter\ifx\csname urlprefix\endcsname\relax\def\urlprefix{URL }\fi

\bibitem{Aho-Sethi-Ullman-86}
A.~Aho, R.~Sethi, J.~Ullman, {C}ompilers: {P}rinciples, {T}echniques and
  {T}ools, Addison-Wesley, Readings, MA, 1986.

\bibitem{Muchnick-97}
S.~Muchnick, {A}dvanced {C}ompiler {D}esign {I}mplementation, Morgan Kaufmann
  Publishers, 1997.

\bibitem{Milner-80}
R.~Milner, {A} {C}alculus of {C}ommunication {S}ystems, Vol.~92 of LNCS,
  Springer, 1980.

\bibitem{Park-81}
D.~Park, {C}oncurrency and {A}utomata on {I}nfinite {S}equences, Theoretical
  Computer Science 104 (1981) 167--183.

\bibitem{Fernandez-Jard-Jeron-92}
J.~Fernandez, C.~Jard, T.~J\'{e}ron, L.~Mounier, ``{O}n the {F}ly''
  {V}erification of {F}inite {T}ransition {S}ystems, Formal Methods in System
  Design .

\bibitem{Godefroid-96}
P.~Godefroid, {P}artial-{O}rder {M}ethods for the {V}erification of
  {C}oncurrent {S}ystems - {A}n {A}pproach to the {S}tate {E}xplosion
  {P}roblem, Vol. 1032 of LNCS, Springer, 1996, iSBN 3-540-60761-7.

\bibitem{McMillan-93}
K.~McMillan, {S}ymbolic {M}odel {C}hecking: an {A}pproach to the {S}tate
  {E}xplosion {P}roblem, Kluwer Academic Publisher, 1993.

\bibitem{Fernandez-Kerbrat-Mounier-93}
J.~Fernandez, A.~Kerbrat, L.~Mounier, {S}ymbolic {E}quivalence {C}hecking, in:
  C.~Courcoubetis (Ed.), Proceedings of CAV'93 (Heraklion, Greece), Vol. 697 of
  LNCS, Springer, 1993, pp. 85--96.

\bibitem{Holzmann-91}
G.~J. Holzmann, {D}esign and {V}alidation of {C}omputer {P}rotocols, Prentice
  Hall Software Series, 1991.

\bibitem{Fernandez-Garavel-Kerbrat-96}
J.~Fernandez, H.~Garavel, A.~Kerbrat, R.~Mateescu, L.~Mounier, M.~Sighireanu,
  {CADP}: {A} {P}rotocol {V}alidation and {V}erification {T}oolbox, in:
  R.~Alur, T.~Henzinger (Eds.), Proceedings of CAV'96 (New Brunswick, USA),
  Vol. 1102 of LNCS, Springer, 1996, pp. 437--440.

\bibitem{Daws-Yovine-96}
C.~Daws, S.~Yovine, {R}educing the {N}umber of {C}lock {V}ariables of {T}imed
  {A}utomata, in: Proceedings of RTSS'96 (Washington, DC, USA), IEEE Computer
  Society Press, 1996.

\bibitem{Kurshan-Levin-98}
R.~Kurshan, V.~Levin, M.~Minea, D.~Peled, H.~Yenig\"un, {S}tatic {P}artial
  {O}rder {R}eduction, in: B.~Steffen (Ed.), Proceedings of TACAS'98 (Lisbon,
  Portugal), Vol. 1384 of LNCS, Springer, 1998, pp. 345--357.

\bibitem{Boigelot-Godefroid-96}
B.~Boigelot, P.~Godefroid, {S}ymbolic {V}erification of {C}ommunication
  {P}rotocols with {I}nfinite {S}tate {S}paces using {QDD}s, in: R.~Alur,
  T.~Henzinger (Eds.), Proceedings of CAV'96 (New Brunswick, USA), Vol. 1102 of
  LNCS, Springer, 1996, pp. 1--12.

\bibitem{Abdulla-Annichini-Bouajjani-98}
P.~Abdulla, A.~Annichini, A.~Bouajjani, {S}ymbolic {V}erification of {L}ossy
  {C}hannel {S}ystems: {A}pplication to the {B}ounded {R}etransmission
  {P}rotocol, in: R.~Cleaveland (Ed.), Proceedings of TACAS'99 (Amsterdam, The
  Netherlands), Vol. 1579 of LNCS, Springer, 1999, pp. 208--222.

\bibitem{Bozga-Fernandez-Ghirvu-98a}
M.~Bozga, J.~Fernandez, L.~Ghirvu, C.~Jard, T.~J\'eron, A.~Kerbrat, P.~Morel,
  L.~Mounier, {V}erification and {T}est {G}eneration for the {SSCOP}
  {P}rotocol, Journal of Science of Computer Programming, Special Isssue on
  Formal Methods in Industry 36~(1) (2000) 27--52.

\bibitem{Jia-Graf-00}
S.~Graf, G.~Jia, {V}erification {E}xperiments on the {M}ascara {P}rotocol, in:
  Proceedings of the SPIN'01 Workshop, 2001, to appear.

\bibitem{Bozga-Fernandez-Ghirvu-99c}
M.~Bozga, J.~Fernandez, L.~Ghirvu, S.~Graf, J.~Krimm, L.~Mounier, {IF}: {A}n
  {I}ntermediate {R}epresentation and {V}alidation {E}nvironment for {T}imed
  {A}synchronous {S}ystems, in: J.~Wing, J.~Woodcock, J.~Davies (Eds.),
  Proceedings of FM'99 (Toulouse, France), Vol. 1708 of LNCS, Springer, 1999,
  pp. 307--327.

\bibitem{Colby-Godefroid-Jagadeesan-98}
C.~Colby, P.~Godefroid, L.~Jagadeesan, {A}utomatically {C}losing {O}pen
  {R}eactive {S}ystems, in: Proceedings of ACM SIGPLAN on Programming Language
  Design and Implementation (Montreal, Canada), 1998, pp. 345--357.

\bibitem{Weiser-84}
M.~Weiser, {P}rogram {S}licing, IEEE Transactions on Software Engineering
  SE-10~(4).

\bibitem{Bozga-Fernandez-Ghirvu-00a}
M.~Bozga, J.-C. Fernandez, L.~Ghirvu, {Using Static Analysis To Improve
  Automatic Test Generation}, in: S.~Graf, M.~Schwartzbach (Eds.), Sixth
  International Conference on Tools and Algorithms for the Construction and
  Analysis of Systems, Vol. 1785 of Lecture Notes in Computer Science,
  Springer, Berlin, DE, 2000, pp. 235--250.

\bibitem{Bensalem-Lakhnech-Owre-98}
S.~Bensalem, Y.~Lakhnech, S.~Owre, {C}omputing {A}bstractions of {I}nfinite
  {S}tate {S}ystems {C}ompositionally and {A}utomatically, in: A.~Hu, M.~Vardi
  (Eds.), Proceedings of CAV'98 (Vancouver, Canada), Vol. 1427 of LNCS,
  Springer, 1998, pp. 319--331.

\end{thebibliography}
