@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:alloywww, key = {{All}}, OPTauthor = {}, title = {{The Alloy model-finding method}}, 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 = {} } @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 = {} } @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:tptp, key = {{TPTP}}, OPTauthor = {}, title = {{Thousands of Problems for Theorem Provers}}, howpublished = {\url{http://www.cs.miami.edu/~tptp}}, 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}, } @article{bib:gheyi, author = {Rohit Gheyi and Tiago Massoni and Paulo Borba}, title = {An Abstract Equivalence Notion for Object Models}, journal = {Electr. Notes Theor. Comput. Sci.}, volume = {130}, year = {2005}, pages = {3-21}, ee = {http://dx.doi.org/10.1016/j.entcs.2005.03.002}, bibsource = {DBLP, http://dblp.uni-trier.de} }