@Article{bib:alloy, author = {Daniel Jackson}, title = {Alloy: a lightweight object modelling notation}, journal = {ACM Transactions on Software Engineering and Methodology}, year = {2002}, OPTkey = {}, volume = {11}, number = {2}, pages = {256--290}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @Book{bib:alloybook, author = {Daniel Jackson}, OPTeditor = {}, title = {Software Abstractions: Logic, Language and Analysis}, publisher = {The MIT Press}, year = {2006}, OPTkey = {}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTaddress = {}, OPTedition = {}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @Misc{bib:aa, key = {{AA}}, OPTauthor = {}, title = {{The Alloy Analyzer}}, howpublished = {\url{http://alloy.mit.edu}}, OPTmonth = {}, OPTyear = {}, OPTnote = {}, OPTannote = {} } @InProceedings{bib:trans, author = {Daniel Jackson}, title = {Automating First-Order Relational Logic}, OPTcrossref = {}, OPTkey = {}, booktitle = {Proceedings of ACM SIGSOFT Conferences on Foundations of Software Engineering}, OPTpages = {}, year = {2000}, OPTeditor = {}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTaddress = {}, month = {11}, OPTorganization = {}, OPTpublisher = {}, OPTnote = {}, OPTannote = {} } @Book{bib:z, author = {J. Michael Spivey}, OPTeditor = {}, title = {The Z notation: a Reference Manual}, publisher = {Prentice Hall}, year = {1992}, OPTkey = {}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTaddress = {}, edition = {2nd edition}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @Book{bib:zref, author = {Jim Woodcock and Jim Davies}, OPTeditor = {}, title = {Using Z: Specification, Refinement and Proof}, publisher = {Prentice Hall}, year = {1996}, OPTkey = {}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTaddress = {}, OPTedition = {}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @Book{bib:specif, author = {Susan Stepney and David Cooper and Jim Woodcock}, OPTeditor = {}, title = {An electronic purse: Specification, Refinement and Proof}, publisher = {Oxford University Computing Laboratory, Programming Research Group}, year = {2000}, OPTkey = {}, OPTvolume = {}, OPTnumber = {}, series = {Technical Monograph PRG--126}, OPTaddress = {}, OPTedition = {}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @Misc{bib:gc, key = {{GC}}, author = {UK Computing Research Commitee}, title = {{Grand Challenges in Computer Research}}, howpublished = {\url{http://www.ukcrc.org.uk/grand_challenges/index.cfm}}, OPTmonth = {}, OPTyear = {}, OPTnote = {}, OPTannote = {} } @Misc{bib:gc6, key = {{GC6}}, OPTauthor = {}, title = {{Grand Challenge 6 : Dependable Systems Evolution}}, howpublished = {\url{http://www.fmnet.info/gc6}}, OPTmonth = {}, OPTyear = {}, OPTnote = {}, OPTannote = {} } @Misc{bib:vsr, key = {{VSR}}, OPTauthor = {}, title = {{VSR-net: A Network for the Verified Software Repository}}, howpublished = {\url{http://www.fmnet.info/gc6}}, OPTmonth = {}, OPTyear = {}, OPTnote = {}, OPTannote = {} } @Article{bib:vsrj, author = {Cliff Jones and Peter O'Hearn and Jim Woodcock}, title = {{Verified Software: A Grand Challenge}}, journal = {Computer}, year = {2006}, OPTkey = {}, volume = {39}, number = {4}, pages = {93--95}, month = {4}, OPTnote = {}, OPTannote = {} } @Unpublished{bib:eves, author = {Leo Freitas and Jim Woodcock}, title = {Mondex in {Z/Eves}}, note = {Slides for the 3rd VSR-net workshop}, OPTkey = {}, month = {5}, year = {2006}, OPTannote = {} } @Misc{bib:eves-www, key = {{ZE}}, OPTauthor = {}, title = {{The Z/Eves System}}, howpublished = {\url{http://nexp.cs.pdx.edu/bart/omse/omse522-winter2002/nfp/sw/z-eves/z-eves.html}}, OPTmonth = {}, OPTyear = {}, OPTnote = {}, OPTannote = {} } @Unpublished{bib:b, author = {Michael Butler and Divakar Yadav}, title = {{Applying Event-B to Mondex}}, note = {Slides for the 3rd VSR-net workshop}, OPTkey = {}, month = {5}, year = {2006}, annote = {University of Southampton} } @Book{bib:bb, author = {Jean-Ren\'e Abrial}, OPTeditor = {}, title = {The B-Book: Assigning Programs to Meanings}, publisher = {Cambridge University Press}, year = {1996}, OPTkey = {}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTaddress = {}, OPTedition = {}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @InProceedings{bib:eventb, author = {Jean-Ren\'e Abrial}, title = {Extending {B} without changing it (for developing distributed systems)}, OPTcrossref = {}, OPTkey = {}, booktitle = {Proceedings of the 1st Conference on the B method}, pages = {169--191}, year = {1996}, OPTeditor = {}, OPTvolume = {}, OPTnumber = {}, series = {Putting into Practice methods and tools for information system design}, OPTaddress = {}, OPTmonth = {}, OPTorganization = {}, publisher = {Habrias}, OPTnote = {}, OPTannote = {} } @TechReport{bib:kiv, author = {Gerhard Schellhorn and Holger Grandy and Dominik Haneberg and Wolfgang Reif}, title = {The Mondex Challenge: Machine-Checked Proofs for an Electronic Purse}, institution = {Lehrstuhl f\"ur Softwaretechnik und Programmiersprachen, Universit\"at Augsburg}, year = {2006}, OPTkey = {}, OPTtype = {}, OPTnumber = {}, OPTaddress = {}, month = {2}, OPTnote = {}, OPTannote = {} } @Misc{bib:kivwww, key = {{KIV}}, OPTauthor = {}, title = {{KIV, the Karlsruhe Interactive Verifier}}, howpublished = {\url{http://i11www.iti.uni-karlsruhe.de/~kiv}}, OPTmonth = {}, OPTyear = {}, OPTnote = {}, OPTannote = {} } @Misc{bib:mondexwww, key = {{MCS}}, OPTauthor = {}, title = {{The Mondex Case Study}}, howpublished = {\url{http://qpq.csl.sri.com/vsr/private/repository/MondexCaseStudy}}, OPTmonth = {}, OPTyear = {}, OPTnote = {}, OPTannote = {} } @Misc{bib:mondexwwwcom, key = {{Mon}}, OPTauthor = {}, title = {{The Mondex electronic purse system}}, howpublished = {\url{http://www.mondex.com}}, OPTmonth = {}, OPTyear = {}, OPTnote = {}, OPTannote = {} } @Misc{bib:moneo, key = {{Mno}}, OPTauthor = {}, title = {{The Moneo electronic purse system}}, howpublished = {\url{http://www.moneo.net}}, OPTmonth = {}, OPTyear = {}, OPTnote = {}, OPTannote = {} } @Unpublished{bib:ocl, author = {Martin Gogolla}, title = {{Use OCL for Mondex}}, note = {Slides for the 3rd VSR-net workshop}, OPTkey = {}, month = {5}, year = {2006}, annote = {University of Bremen} } @Article{bib:oclj, author = {Jos Warmer and Anneke Kleppe}, title = {{OCL: The constraint language of the UML}}, journal = {Journal of Object-Oriented Programming}, year = {1999}, OPTkey = {}, volume = {12}, OPTnumber = {}, pages = {10--13}, month = {3}, OPTnote = {}, OPTannote = {} } @Article{bib:pdp, author = {David Crocker and Judith Carlton}, title = {{Perfect Developer: what it is and what it does}}, journal = {FACS Facts: Newsletter of the BCS Formal Aspects of Computer Science special interest group}, year = {2004}, OPTkey = {}, OPTvolume = {}, OPTnumber = {}, OPTpages = {}, month = {11}, OPTnote = {}, OPTannote = {} } @Misc{bib:pdwww, key = {{PD}}, OPTauthor = {}, title = {{Perfect Developer}}, howpublished = {\url{http://www.eschertech.com}}, OPTmonth = {}, OPTyear = {}, OPTnote = {}, OPTannote = {} } @Unpublished{bib:pd, author = {David Crocker}, title = {{Mondex Revisited with Perfect Developer}}, note = {{Slides for the 2nd VSR-net Workshop}}, OPTkey = {}, month = {1}, year = {2006}, OPTannote = {} } @Misc{bib:coq, key = {{Coq}}, OPTauthor = {}, title = {{The Coq proof assistant}}, howpublished = {\url{http://coq.inria.fr}}, OPTmonth = {}, OPTyear = {}, OPTnote = {}, OPTannote = {} } @Unpublished{bib:vdm, author = {Cliff Jones}, title = {{VSR Mondex Meeting}}, note = {Slides of the 2nd VSR-net Workshop}, OPTkey = {}, month = {1}, year = {2006}, OPTannote = {} } @Book{bib:vdmb, author = {Cliff Jones}, OPTeditor = {}, title = {Systematic Software Development using VDM}, publisher = {Prentice Hall}, year = {1990}, OPTkey = {}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTaddress = {}, OPTedition = {}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @Unpublished{bib:raise, author = {Chris George and Anne Haxthausen}, title = {{Specification and Proof of the Mondex Electronic Purse}}, note = {Slides of the 3rd VSR-net Workshop}, OPTkey = {}, month = {5}, year = {2006}, OPTannote = {} } @Book{bib:raiseb, author = {Chris George and Anne E. Haxthausen and Steven Hughes and Robert Milae and Soren Prehn and Jan Storbank Pedersen}, OPTeditor = {}, title = {The RAISE Development Method}, publisher = {Prentice Hall}, year = {1995}, OPTkey = {}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTaddress = {}, OPTedition = {}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @InProceedings{bib:prioni, author = {Konstantine Arkoudas and Sarfraz Khurshid and Darko Marinov and Martin Rinard}, title = {{Integrating Model-Checking and Theorem Proving for Relational Reasoning}}, OPTcrossref = {}, OPTkey = {}, booktitle = {7th International Seminar on Relational Methods in Computer Science (RelMiCS)}, OPTpages = {}, year = {2003}, OPTeditor = {}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTaddress = {}, OPTmonth = {}, OPTorganization = {}, OPTpublisher = {}, OPTnote = {}, OPTannote = {} } @Misc{bib:athena, key = {{Ath}}, OPTauthor = {}, title = {{The Athena interactive theorem proving system}}, howpublished = {\url{http://www.cag.csail.mit.edu/~kostas/dpls/athena}}, OPTmonth = {}, OPTyear = {}, OPTnote = {}, OPTannote = {} } @Misc{bib:ocaml, key = {{OCa}}, OPTauthor = {}, title = {{The Objective Caml functional programming language}}, howpublished = {\url{http://caml.inria.fr/ocaml}}, OPTmonth = {}, OPTyear = {}, OPTnote = {}, OPTannote = {} } @Misc{bib:tptp, key = {{TPTP}}, OPTauthor = {}, title = {{Thousands of Problems for Theorem Provers}}, howpublished = {\url{http://www.cs.miami.edu/~tptp}}, OPTmonth = {}, OPTyear = {}, OPTnote = {}, OPTannote = {} } @Misc{bib:e, key = {{E}}, OPTauthor = {}, title = {{The E Equational Theorem Prover}}, howpublished = {\url{http://www4.in.tum.de/~schulz/WORK/eprover.html}}, OPTmonth = {}, OPTyear = {}, OPTnote = {}, OPTannote = {} } @Misc{bib:spass, key = {{Spass}}, OPTauthor = {}, title = {{SPASS: An Automated Theorem Prover for First-Order Logic with Equality}}, howpublished = {\url{http://spass.mpi-sb.mpg.de}}, OPTmonth = {}, OPTyear = {}, OPTnote = {}, OPTannote = {} } @Article{bib:smt, author = {Lee Momtahan}, title = {{Towards a Small Model Theorem for Data Independent Systems}}, journal = {Electronic Notes in Theoretical Computer Science}, year = {2004}, OPTkey = {}, volume = {128}, number = {6}, OPTpages = {}, month = {3}, OPTnote = {}, OPTannote = {} } @InProceedings{bib:tcfol, author = {Tal Lev-Ami and Neil Immerman and Thomas W. Reps and Shmuel Sagiv and S Srivastava and Greta Yorsh}, title = {{Simulating Reachability Using First-Order Logic with Applications to Verification of Linked Data Structures}}, OPTcrossref = {}, OPTkey = {}, booktitle = {Proceedings of 20th International Conference on Automated Deduction}, pages = {99--115}, year = {2005}, OPTeditor = {}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTaddress = {}, OPTmonth = {}, OPTorganization = {}, OPTpublisher = {}, OPTnote = {}, OPTannote = {} } @InProceedings{bib:ooz, author = {Anthony Hall}, title = {{Using Z as a Specification Calculus for Object-oriented Systems}}, OPTcrossref = {}, OPTkey = {}, booktitle = {VDM90 : VDM and Z Formal Methods in Software Development, Lecture Notes in Computer Science}, pages = {290--318}, year = {1990}, OPTeditor = {}, OPTvolume = {}, number = {428}, OPTseries = {}, OPTaddress = {}, OPTmonth = {}, OPTorganization = {}, OPTpublisher = {}, OPTnote = {}, OPTannote = {} } @InProceedings{bib:kodkod, title = {Kodkod: A Relational Model Finder.}, author = {Emina Torlak and Daniel Jackson}, booktitle = {TACAS}, OPTcrossref = {}, editor = {Orna Grumberg and Michael Huth}, pages = {632--647}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, url = {http://dblp.uni-trier.de/db/conf/tacas/tacas2007.html#TorlakJ07}, volume = {4424}, year = {2007}, biburl = {http://www.bibsonomy.org/bibtex/2ff7b0b18e74fbcc8b56fd888324d6245/dblp}, description = {dblp}, ee = {http://dx.doi.org/10.1007/978-3-540-71209-1_49}, isbn = {978-3-540-71208-4}, date = {2007-07-31}, keywords = {dblp } } @Misc{bib:kodkodwww, OPTkey = {}, author = {Emina Torlak}, title = {{Kodkod, model finder for first order relational logic}}, howpublished = {\url{http://web.mit.edu/emina/www/kodkod.html}}, OPTmonth = {}, OPTyear = {}, OPTnote = {}, OPTannote = {} } @TechReport{bib:mondextech, author = {Tahina Ramananandro}, title = {{Mondex, an electronic purse : specification and refinement checks with the Alloy model-finding method}}, institution = {MIT and \'Ecole normale sup\'erieure}, year = {2006}, OPTkey = {}, type = {Internship report}, OPTnumber = {}, OPTaddress = {}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @Misc{bib:mondextechwww, OPTkey = {}, author = {Tahina Ramananandro}, title = {{The Mondex Case Study with Alloy}}, howpublished = {\url{http://www.eleves.ens.fr/~ramanana/work/mondex}}, OPTmonth = {}, OPTyear = {}, OPTnote = {}, OPTannote = {} } @article{bib:frias, author = {Marcelo F. Frias and Carlos G. L\'{o}pez Pombo and Gabriel A. Baum and Nazareno M. Aguirre and Thomas S. E. Maibaum}, title = {Reasoning about static and dynamic properties in alloy: A purely relational approach}, journal = {ACM Trans. Softw. Eng. Methodol.}, volume = {14}, number = {4}, year = {2005}, issn = {1049-331X}, pages = {478--526}, doi = {http://doi.acm.org/10.1145/1101815.1101819}, publisher = {ACM}, address = {New York, NY, USA}, }