Yes. That's the symbolic execution approach to verification. At each IF, there's another set of future paths to explore, with more constraints on the variables. The Microsoft Static Driver Verifier is said to work that way.[1] It's mostly automatic, but slow. It made OS crashes caused by Windows drivers mostly a thing of the past in Windows 7.

[1] https://www.microsoft.com/en-us/research/wp-content/uploads/...