The content of this page is only available in German.
Please go to German version of this page

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.