\newcommand{\etalchar}[1]{$^{#1}$}
\begin{thebibliography}{LAIR{\etalchar{+}}05}

\bibitem[{AA}]{bib:aa}
{The Alloy Analyzer}.
\newblock \url{http://alloy.mit.edu}.

\bibitem[AKMR03]{bib:prioni}
Konstantine Arkoudas, Sarfraz Khurshid, Darko Marinov, and Martin Rinard.
\newblock {Integrating Model-Checking and Theorem Proving for Relational
  Reasoning}.
\newblock In {\em 7th International Seminar on Relational Methods in Computer
  Science (RelMiCS)}, 2003.

\bibitem[{Ath}]{bib:athena}
{The Athena interactive theorem proving system}.
\newblock \url{http://www.cag.csail.mit.edu/~kostas/dpls/athena}.

\bibitem[FPB{\etalchar{+}}05]{bib:frias}
Marcelo~F. Frias, Carlos G.~L\'{o}pez Pombo, Gabriel~A. Baum, Nazareno~M.
  Aguirre, and Thomas S.~E. Maibaum.
\newblock Reasoning about static and dynamic properties in alloy: A purely
  relational approach.
\newblock {\em ACM Trans. Softw. Eng. Methodol.}, 14(4):478--526, 2005.

\bibitem[FW06]{bib:eves}
Leo Freitas and Jim Woodcock.
\newblock Mondex in {Z/Eves}.
\newblock Slides for the 3rd VSR-net workshop, 5 2006.

\bibitem[Hal90]{bib:ooz}
Anthony Hall.
\newblock {Using Z as a Specification Calculus for Object-oriented Systems}.
\newblock In {\em VDM90 : VDM and Z Formal Methods in Software Development,
  Lecture Notes in Computer Science}, number 428, pages 290--318, 1990.

\bibitem[Jac00]{bib:trans}
Daniel Jackson.
\newblock Automating first-order relational logic.
\newblock In {\em Proceedings of ACM SIGSOFT Conferences on Foundations of
  Software Engineering}, 11 2000.

\bibitem[Jac02]{bib:alloy}
Daniel Jackson.
\newblock Alloy: a lightweight object modelling notation.
\newblock {\em ACM Transactions on Software Engineering and Methodology},
  11(2):256--290, 2002.

\bibitem[Jac06]{bib:alloybook}
Daniel Jackson.
\newblock {\em Software Abstractions: Logic, Language and Analysis}.
\newblock The MIT Press, 2006.

\bibitem[LAIR{\etalchar{+}}05]{bib:tcfol}
Tal Lev-Ami, Neil Immerman, Thomas~W. Reps, Shmuel Sagiv, S~Srivastava, and
  Greta Yorsh.
\newblock {Simulating Reachability Using First-Order Logic with Applications to
  Verification of Linked Data Structures}.
\newblock In {\em Proceedings of 20th International Conference on Automated
  Deduction}, pages 99--115, 2005.

\bibitem[{MCS}]{bib:mondexwww}
{The Mondex Case Study}.
\newblock \url{http://qpq.csl.sri.com/vsr/private/repository/MondexCaseStudy}.

\bibitem[Mom04]{bib:smt}
Lee Momtahan.
\newblock {Towards a Small Model Theorem for Data Independent Systems}.
\newblock {\em Electronic Notes in Theoretical Computer Science}, 128(6), 3
  2004.

\bibitem[{Mon}]{bib:mondexwwwcom}
{The Mondex electronic purse system}.
\newblock \url{http://www.mondex.com}.

\bibitem[Ram]{bib:mondextechwww}
Tahina Ramananandro.
\newblock {The Mondex Case Study with Alloy}.
\newblock \url{http://www.eleves.ens.fr/~ramanana/work/mondex}.

\bibitem[Ram06]{bib:mondextech}
Tahina Ramananandro.
\newblock {Mondex, an electronic purse : specification and refinement checks
  with the Alloy model-finding method}.
\newblock Internship report, MIT and \'Ecole normale sup\'erieure, 2006.

\bibitem[SCW00]{bib:specif}
Susan Stepney, David Cooper, and Jim Woodcock.
\newblock {\em An electronic purse: Specification, Refinement and Proof}.
\newblock Technical Monograph PRG--126. Oxford University Computing Laboratory,
  Programming Research Group, 2000.

\bibitem[SGHR06]{bib:kiv}
Gerhard Schellhorn, Holger Grandy, Dominik Haneberg, and Wolfgang Reif.
\newblock The mondex challenge: Machine-checked proofs for an electronic purse.
\newblock Technical report, Lehrstuhl f\"ur Softwaretechnik und
  Programmiersprachen, Universit\"at Augsburg, 2 2006.

\bibitem[Spi92]{bib:z}
J.~Michael Spivey.
\newblock {\em The Z notation: a Reference Manual}.
\newblock Prentice Hall, 2nd edition edition, 1992.

\bibitem[TJ07]{bib:kodkod}
Emina Torlak and Daniel Jackson.
\newblock Kodkod: A relational model finder.
\newblock In Orna Grumberg and Michael Huth, editors, {\em TACAS}, volume 4424
  of {\em Lecture Notes in Computer Science}, pages 632--647. Springer, 2007.

\bibitem[Tor]{bib:kodkodwww}
Emina Torlak.
\newblock {Kodkod, model finder for first order relational logic}.
\newblock \url{http://web.mit.edu/emina/www/kodkod.html}.

\bibitem[{TPT}]{bib:tptp}
{Thousands of Problems for Theorem Provers}.
\newblock \url{http://www.cs.miami.edu/~tptp}.

\bibitem[WD96]{bib:zref}
Jim Woodcock and Jim Davies.
\newblock {\em Using Z: Specification, Refinement and Proof}.
\newblock Prentice Hall, 1996.

\end{thebibliography}