Does this use tactics to identify contradictions, tautologies, subsumptions, etc in conditions? How does this work?
Very briefly, the analysis tries to approximate the "states space" for the program, and if it intersect problematic value then it detects a bug. For example, if it can approximate the range of values a variable "x" can take, and this range includes 0 and x is used for division, then a division by zero bug can happen.
When an issue is found, those tools can give you the detailed path leading to the bug, from input down to a call chain to the bug.
The challenge here is to find a good approximation of the possible states. If the tool over-approximate, there will be false alarms. If it under approximate, it will miss bugs. Most tools do a bit of both ;)