Mechanising Mondex with Z/Eves
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 specification and some 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 Repository for the Verified Software Grand Challenge.
mondex refinement correctness grand challenges electronic finance grand challenge in verified software security smart cards software archaeology theorem proving verification verified software repository z /eves z notation