Precise and Automated Contract-based Reasoning for Verification and Certification of Information Flow Properties of Programs wit