Statically verifying behavioral properties of programs is an important research problem. An efficient solution to this problem will have visible effects over multiple domains, ranging from program development, program ...