Extensive support for information flow verification
- Verification of ordinary non-interference for sequential programs
- Verification of possibilistic and probabilistic non-interference for concurrent programs
- Counterexamples for non-interference proofs