{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T17:49:24Z","timestamp":1725472164210},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540488156"},{"type":"electronic","value":"9783540488163"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11921240_2","type":"book-chapter","created":{"date-parts":[[2006,11,2]],"date-time":"2006-11-02T13:28:19Z","timestamp":1162474099000},"page":"15-34","source":"Crossref","is-referenced-by-count":8,"title":["Z\/Eves and the Mondex Electronic Purse"],"prefix":"10.1007","author":[{"given":"Jim","family":"Woodcock","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Leo","family":"Freitas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"2_CR1","first-page":"143","volume":"18","author":"J. Bicarregui","year":"2006","unstructured":"Bicarregui, J., Hoare, T., Woodcock, J.: The verified software repository: a step towards the verifying compiler. FACJ\u00a018(2), 143\u2013151 (2006)","journal-title":"FACJ"},{"key":"2_CR2","unstructured":"Cooper, D., Stepney, S., Woodcock, J.: Derivation of Z Refinement Proof Rules. Technical Report YCS-2002-347, University of York (December 2002)"},{"key":"2_CR3","unstructured":"Crocker, D.: Safe object-oriented software:\u00a0the verified design-by-contract paradigm. In: Redmill, F., Anderson, T. (eds.) Practical Elements of Safety:\u00a0Proceedings of the 12th Safety-Critical Systems Symposium. Springer, Heidelberg"},{"key":"2_CR4","series-title":"FACIT (Formal Approaches to Computing and Information Technology) series","volume-title":"Specification Case Studies in RAISE","year":"2002","unstructured":"Van Dang, H., George, C., Janowski, T., Moore, R. (eds.): Specification Case Studies in RAISE. FACIT (Formal Approaches to Computing and Information Technology) series. Springer, Heidelberg (2002)"},{"key":"2_CR5","unstructured":"ITSEC. Information Technology Security Evaluation Criteria (ITSEC): Preliminary Harmonised Criteria. Document COM(90) 314, Version 1.2. Commission of the European Communities (1991)"},{"key":"2_CR6","first-page":"350","volume-title":"Software Abstractions:\u00a0Logic, Language, and Analysis","author":"D. Jackson","year":"2006","unstructured":"Jackson, D.: Software Abstractions:\u00a0Logic, Language, and Analysis, p. 350. The MIT Press, Cambridge (2006)"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Jackson, D.: Dependable Software by Design. Scientific American (June 2006)","DOI":"10.1038\/scientificamerican0606-68"},{"issue":"4","key":"2_CR8","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1109\/MC.2006.145","volume":"39","author":"C. Jones","year":"2006","unstructured":"Jones, C., O\u2019Hearn, P., Woodcock, J.: Verified Software: A Grand Challenge. IEEE Computer\u00a039(4), 93\u201395 (2006)","journal-title":"IEEE Computer"},{"key":"2_CR9","unstructured":"M\u00e9tayer, C., Abrial, J.-R., Voisin, L.: Event-B Language. Project IST-511599 RODIN Rigorous Open Development Environment for Complex Systems. RODIN Deliverable 3.2 Public Document, May 31 (2005), rodin.cs.ncl.ac.uk"},{"key":"2_CR10","unstructured":"UML 2.0 OCL Specification. OMG Adopted Specification ptc\/03-10-14 (2004)"},{"key":"2_CR11","unstructured":"Mondex smart cards, http:\/\/www.mondex.com"},{"key":"2_CR12","unstructured":"The QPQ Deductive Software Repository, qpq.csl.sri.com"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Saaltink, M.: The Z\/EVES User\u2019s Guide, ORA Canada (1997)","DOI":"10.1007\/BFb0027284"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0027284","volume-title":"ZUM\u201997: The Z Formal Specification Notation","author":"M. Saaltink","year":"1997","unstructured":"Saaltink, M.: The Z\/EVES System. In: Till, D., Bowen, J.P., Hinchey, M.G. (eds.) ZUM 1997. LNCS, vol.\u00a01212, Springer, Heidelberg (1997)"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Schellhorn, G., Grandy, H., Haneberg, D., Reif, W.: The Mondex Challenge: Machine Checked Proofs for an Electronic Purse. Technical Report. Institute of Computer Science, University of Augsburg (2006)","DOI":"10.1007\/11813040_2"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/11813040_2","volume-title":"FM 2006: Formal Methods","author":"G. Schellhorn","year":"2006","unstructured":"Schellhorn, G., Grandy, H., Haneberg, D., Reif, W.: The Mondex Challenge: Machine Checked Proofs for an Electronic Purse. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol.\u00a04085, pp. 16\u201331. Springer, Heidelberg (2006)"},{"key":"2_CR17","series-title":"Prentice Hall International Series in Computer Science","first-page":"150","volume-title":"The Z Notation:\u00a0A Reference Manual","author":"J.M. Spivey","year":"1992","unstructured":"Spivey, J.M.: The Z Notation:\u00a0A Reference Manual, 2nd edn. Prentice Hall International Series in Computer Science, p. 150. Prentice-Hall, Englewood Cliffs (1992)","edition":"2"},{"key":"2_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/978-3-540-49676-2_20","volume-title":"ZUM \u201998: The Z Formal Specification Notation","author":"S. Stepney","year":"1998","unstructured":"Stepney, S., Cooper, D., Woodcock, J.: More Powerful Z Data Refinement: Pushing the State of the Art in Industrial Refinement. In: Bowen, J.P., Fett, A., Hinchey, M.G. (eds.) ZUM 1998. LNCS, vol.\u00a01493, pp. 284\u2013309. Springer, Heidelberg (1998)"},{"key":"2_CR19","series-title":"EWICS","volume-title":"BCS-FACS Third Northern Formal Methods Workshop","author":"S. Stepney","year":"1998","unstructured":"Stepney, S.: A Tale of Two Proofs. In: BCS-FACS Third Northern Formal Methods Workshop, Ilkley, September 1998. EWICS. Springer, Heidelberg (1998)"},{"key":"2_CR20","unstructured":"Stepney, S., Cooper, D., Woodcock, J.: An Electronic Purse: Specification, Refinement, and Proof. Technical Monograph PRG-126, Oxford University Computing Laboratory (July 2000)"},{"key":"2_CR21","unstructured":"Woodcock, J., Davies, J.: Using Z:\u00a0Specification, Refinement, and Proof. Prentice Hall International Series in Computer Science, p. 391. Prentice Hall, Englewood Cliffs (1996), The complete text is available from: http:\/\/www.usingz.com"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing - ICTAC 2006"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11921240_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T19:59:00Z","timestamp":1605643140000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11921240_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540488156","9783540488163"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/11921240_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}