A formal proof of the Chip Model Channel Separation Property

Programatica meeting presentation by Thomas Hallgren, May 11, 2004


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.

Thomas Hallgren
Programatica Tool Talks
Programatica Tools