« May 2017 »
May
MoTuWeThFrSaSu
1234567
891011121314
15161718192021
22232425262728
293031
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