Z/Eves and the Mondex Electronic Purse

DOI10.1007/11921240_2zbMath1168.68544OpenAlexW1582995952MaRDI QIDQ3525137

Leo Freitas, J. C. P. Woodcock

Publication date: 11 September 2008

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/11921240_2

zbMATH Keywords

theorem provingsecurityrefinementsmart cardsZ/Evesgrand challengeverified software repositoryelectronic financemondexsoftware archaeologythe Z notation

Mathematics Subject Classification ID

Related Items (5)

Using formal reasoning on a model of tasks for FreeRTOS ⋮ JCML: A specification language for the runtime verification of Java card programs ⋮ Verifying the CICS file control API with Z/Eves: An experiment in the verified software repository ⋮ Mechanising a formal model of flash memory ⋮ POSIX file store in Z/Eves: An experiment in the verified software repository

Uses Software

• Z/EVES

This page was built for publication: Z/Eves and the Mondex Electronic Purse