AVA

A verifier for approximations of transcendental functions.

A certificate checker for roundoff error bounds

A new, nondeterministic floating-point source semantics and a proof-of-concept connection to the CakeML verified compiler.

The benchmark repository for the added float support to the KeY deductive verifier.

This is a static analyser developed for the Program Analysis course at TU Kaiserslautern. for more information see the course page: https://moodle.mpi-sws.org/course/view.php?id=24