Referee

Referee is a deductive verifier.This means that we check for a program annotated with invariants, if the invariants are sufficient for an inductive proof. For example, for a loop invariant we check if it holds at the beginning of the loop, if it is preserved by the loop body and if it is strong enough the prove the remaining program after the loop correct. These annotated invariants can be extracted from correctness witnesses, therefore Referee can be used as a validator for these.

Web Interface

Referee is available via a web interface.