A formal proof of the Chip Model Channel Separation Property

Programatica meeting presentation by Thomas Hallgren, May 11, 2004

• All slides in one page
• Table of contents
• Slides
• Source files (The .alfa text files are not very readable. View them in Alfa!)

Abstract

This is a follow-up to my February talk on the Channel Separation proof in Alfa.

This time, the Chip Model is expressed in Haskell, and the properties of interest are expressed as P-Logic assertions in the Haskell code. The Alfa certificate server translates the Haskell code to Alfa and allows proofs constructed in Alfa to be captured in certificates and attached as evidence for the validity of the P-Logic assertions.

The Alfa proofs are still the only formally verified proofs of the Chip Model Separation property.