Specification of a Smart Card Operating System

Gustavo Betarte, Cristina Cornes, Nora Szasz, Alvaro Tasistro.
In this page we make available documentation concerning the specification of (a version of) an operating system of a Smart Card. 
Contents
  • Specification of a Smart Card Operating System .

    • Informal specification of a smart card of (a modified version of) profile P. By informal here we mean that it has been written down in a rigorous mathematical language but no machine-assisted verification was performed on it.
     
     
  • Specification of a Smart Card Operating System in Coq  (zipped files with Coq source files  and Coq source files in Html format)

    • A machine-verified version of the specification and some properties developed using the proof-assistant Coq.
    The smart card group at InCo

    Last modified: Fri Oct 8 15:26:46 GMT 1999