Proving Unrealizability - Verifying Infinitely Many Programs at Once

Explore a 37-minute lecture by Loris D'Antoni from the University of Wisconsin - Madison, presented at the Simons Institute as part of the Synthesis of Models and Systems series. Delve into the concept of proving unrealizability in program verification, which involves verifying properties for an infinite set of programs simultaneously. Discover how this approach differs from traditional program verification and its applications in various domains, including synthesis problem specifications, reasoning about partially specified code, and self-modifying code. Learn about recent advancements in designing systems capable of verifying properties across infinitely many programs, offering insights into this complex area of computer science research.

Proving Unrealizability (aka Verifying Infinitely Many Programs at Once)