1. One or more computer-readable media including computer-executable instructions for verifying a program, comprising: converting a programming language of the program into an intermediate language; eliminating loops within the program represented by the intermediate language such that the program corresponds to an acyclic intermediate language representation of the program; converting the program from the acyclic intermediate language representation into a passive, acyclic intermediate language representation; determining dominators for the passive, acyclic intermediate language representation of the program; and generating a verification condition from the passive, acyclic intermediate language representation of the program, wherein the verification condition is structured according to the computed dominators such that when a theorem prover identifies a potential error, portions of the passive, acyclic intermediate language representation of the program irrelevant to the potential error are ignored.