In ALBIA we develop a verifier for IF properties as well as the exploit generation tool KEG. Below you find two prototypes of these tools:

• Standalone Verifier for IF Properties: The standalone verifier automatically generates loop invariants using a novel approach on integrating abstraction into a logic framework. A webstart of the standalone verifier can be downloaded here.

• Exploit Generation : Generates exploits for information leaks. Supported Policies: non-interference and delimited information release. Click here for more details.