Output details
11 - Computer Science and Informatics
Newcastle University
Mechanising Mondex with Z/Eves
<10> Mondex smartcards represented the first EAL7 certified-product, the highest assurance level by international standards, requiring proofs from specification to design to code. This work kick-started the Software Verification Grand Challenge with eight teams using different formalisms, and it took 250 pages of Z specifications. Four residual errors were found and fixed. Its effort served as a comparative measure between methods that has not been performed before. Interestingly, other teams working on simplified versions found most errors. The result: a reference proof and large-scale proof engineering techniques transferred across other GC experiments, and eight other formal methodologies.