[SAS23] Verifying Infinitely Many Programs at Once

[SAS23] Verifying Infinitely Many Programs at Once

Loris D'Antoni

In traditional program verification, the goal is to automati- cally 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 φ, one needs to verify that all programs in the search space are incorrect, e.g., satisfy the property ¬φ. 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