« July 2017 »
July
MoTuWeThFrSaSu
12
3456789
10111213141516
17181920212223
24252627282930
31
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