« June 2017 »
June
MoTuWeThFrSaSu
1234
567891011
12131415161718
19202122232425
2627282930
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