{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,10]],"date-time":"2026-11-10T22:26:55Z","timestamp":1794349615047,"version":"4.9.0"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540732099","type":"print"},{"value":"9783540732105","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73210-5_21","type":"book-chapter","created":{"date-parts":[[2007,9,13]],"date-time":"2007-09-13T00:03:05Z","timestamp":1189641785000},"page":"393-412","source":"Crossref","is-referenced-by-count":7,"title":["Algebraic Approaches to Formal Analysis of the Mondex Electronic Purse System"],"prefix":"10.1007","author":[{"given":"Weiqiang","family":"Kong","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kazuhiro","family":"Ogata","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kokichi","family":"Futatsugi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"21_CR1","unstructured":"MasterCard International Inc. Mondex. URL: http:\/\/www.mondex.com\/."},{"key":"21_CR2","unstructured":"Mondex Case Study. URL: http:\/\/qpq.csl.sri.com\/vsr\/private\/repository\/MondexCaseStudy"},{"key":"21_CR3","unstructured":"UK Computing Research Committee, Grand Challenges in Computer Research. URL: http:\/\/www.ukcrc.org.uk\/grand_challenges\/index.cfm"},{"key":"21_CR4","unstructured":"Woodcock, J.: Grand Challenges 6: Dependable Systems Evolution. URL: http:\/\/www.fmnet.info\/gc6\/"},{"key":"21_CR5","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, University of Augsburg (2006)","DOI":"10.1007\/11813040_2"},{"key":"21_CR6","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":"21_CR7","unstructured":"Haxthausen, A., George, C., Sch\u00fctz, M.: Specification and proof of the Mondex electronic purse. In: AWCVS 2006, UNU-IIST Report No. 347, pp. 209\u2013224 ( 2006)"},{"key":"21_CR8","doi-asserted-by":"crossref","unstructured":"Ramananandro, T.: Mondex, An Electronic Purse: Specification and refinement checks with the Alloy model-finding method. Internship Report (2006), http:\/\/www.eleves.ens.fr\/home\/ramanana\/work\/mondex\/","DOI":"10.1007\/s00165-007-0058-z"},{"key":"21_CR9","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":"21_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"170","DOI":"10.1007\/978-3-540-39958-2_12","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"K. Ogata","year":"2003","unstructured":"Ogata, K., Futatsugi, K.: Proof scores in the OTS\/CafeOBJ method. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol.\u00a02884, pp. 170\u2013184. Springer, Heidelberg (2003)"},{"key":"21_CR11","unstructured":"CafeOBJ Web Site (2007), URL: http:\/\/www.ldl.jaist.ac.jp\/cafeobj\/"},{"key":"21_CR12","volume-title":"CafeOBJ report. AMAST Series in Computing","author":"R. Diaconescu","year":"1998","unstructured":"Diaconescu, R., Futatsugi, R.K.: CafeOBJ report. AMAST Series in Computing, vol.\u00a06. World Scientific, Singapore (1998)"},{"key":"21_CR13","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: Maude manual (Version 2.2) (2007), URL: http:\/\/maude.cs.uiuc.edu\/maude2-manual\/"},{"key":"21_CR14","unstructured":"Nakamura, M., Kong, W., Ogata, K., Futatsugi, K.: A complete specification translation from OTS\/CafeOBJ into OTS\/Maude. In: IEICE TR, SS2006, vol.\u00a013, pp. 1\u20136 (2006)"},{"key":"21_CR15","first-page":"59","volume-title":"APSEC 2005","author":"W. Kong","year":"2005","unstructured":"Kong, W., Ogata, K., Futatsugi, K.: A lightweight integration of theorem proving and model checking for system verification. In: APSEC 2005, pp. 59\u201366. IEEE CS, Washington, DC (2005)"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73210-5_21.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T06:05:42Z","timestamp":1619503542000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73210-5_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540732099","9783540732105"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73210-5_21","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-540-73210-5","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}