A piece of code in a computer program is infeasible if it cannot be part of any normally-terminating execution of the program. We develop an algorithm for the automatic detection o...
Motivated by the problem of deciding verification conditions for the verification of functional programs, we present new decision procedures for automated reasoning about functio...