A Proof of the Chip Model Separation Property in Alfa

Programatica meeting presentation by Thomas Hallgren, February 27, 2004

• All slides in one page
• Slides
• Alfa source files (ASCII text files, not very readable. View them in Alfa!)

Abstract

This talk presents the first formally verified proof of the Channel Separation property for the Chip Model.

The Chip Model (loosely based on the Motorola AIM chip) was formulated early on in the Programatica project as an example of using Haskell as a hardware modelling example and to serve as a case study illustrating the applicability of the Programatica approach to high assurance and formal verification.

This talk presents a reformulation of the Chip Model in Alfa and a proof of the desired Channel Separation property. It does not make any use of the Programatica tools, but instead illustrates the power of propositions-as-types and other language features that allow the model (and the proofs) to be expressed in a more modular way than they could have been in Haskell.