« March 2017 »
March
MoTuWeThFrSaSu
12345
6789101112
13141516171819
20212223242526
2728293031
Uni-Logo
You are here: Home Tools Exorcise
Document Actions

Exorcise

Exorcise closes the gap between static analysis used in modern compilers and state of the art formal methods. It produces precise and intuitive compiler-like error messages (i.e., it never generates false alarms) and detects even sophisticated errors and certain cases of non-termination by analyzing the entire state space of the program. Exorcise detects doomed program points which are expressions or statements in a program that cannot be executed (i.e., they either crash the program or are unreachable) due to contradictions in the control flow or specification.

Personal tools