Proving Unrealizability (aka Verifying Infinitely Many Programs at Once)

In traditional program verification, the goal is to automatically prove whether a program meets a given property. However, in some cases one might need to prove that a (potentially infinite) set of programs meets a given property. For example, to establish that no program in a set of possible programs (i.e., a search space) is a valid solution to a synthesis problem specification, e.g., a property phi, one needs to verify that all programs in the search space are incorrect, e.g., satisfy the property not(phi). The need to verify multiple programs at once also arises in other domains such as reasoning about partially specified code (e.g., in the presence of library functions) and self-modifying code. This paper discusses our recent work in designing systems for verifying properties of infinitely many programs at once