By the same authors

Z/eyes and the Mondex Electronic Purse

Research output: Chapter in Book/Report/Conference proceedingChapter



Publication details

Title of host publicationTHEORETICAL ASPECTS OF COMPUTING - ICTAC 2006
DatePublished - 2006
Number of pages20
Place of PublicationBERLIN
Original languageEnglish


We describe our experiences in mechanising the specification, refinement, and proof of the Mondex Electronic Purse using the Z/Eves theorem prover. We took a conservative approach and mechanised the original LATEX sources, without changing their technical content, except to correct errors: we found problems in the original texts and missing invariants in the refinements. Based on these experiences, we present novel and detailed guidance on how to drive Z/Eves successfully. The work contributes to the research objectives of building the Repository for the Verified Software Grand Challenge.

    Research areas

  • electronic finance, Grand Challenge, Mondex, refinement, security, smart cards, software archaeology, theorem proving, Verified Software Repository, the Z notation, Z/Eves

Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations