SeaHorn can be used to prove termination and non-termination of programs. The core of the approach lies on the innovative use of the backend verification engines to build termination arguments. More specifically, the backend verification engines are used to systematically sample terminating program execution and to extrapolate from these a candidate ranking function for the program. The candidate ranking function can be a piecewise-defined, lexicographic, or multiphase combination of affine functions of the program variables. The backend verification engines are then used to validate the candidate ranking function, or to otherwise provide a witness for program non-termination. More information about this can be found this paper.

Inconsistent code is an important class of program abnormalities that appears in real-world code bases and often reveals serious bugs. A piece of code is inconsistent if it is not part of any safely terminating execution. Existing approaches to inconsistent code detection scale to programs with millions of lines of code, and have lead to patches in applications like the web-server Tomcat or the Linux kernel. However, the ability of existing tools to detect inconsistencies is limited by gross over-approximation of looping control-flow. SeaHorn is able to detect inconsistent code fragments. This is done by computing a path coverage for the generated system of Horn clauses. More information about this can be found in this paper.