Pointers
The code is in the Programatica CVS repository:
programatica/examples/ChannelSeparation/Alfa
- Chip model, properties and proofs expressed entirely in Alfa.
programatica/examples/ChannelSeparation/Alfa/Haskell
- Chip model in Haskell,
- properties expressed as P-Logic assertions,
- Alfa certificates associating proof in Alfa to the asserted properties.