Automating Unrealizability Logic: Hoare-Style Proof Synthesis for Infinite Sets of Programs

TL;DR

This paper introduces Wuldo, a Hoare-style proof synthesis tool for Unrealizability Logic that automates reasoning about infinite sets of programs, enabling reusable insights and faster verification.

Contribution

It presents the first UL proof synthesis algorithm, Wuldo, which can synthesize and reuse nonterminal summaries to verify infinite program sets more efficiently.

Findings

Wuldo can prove properties of infinitely many programs.

Wuldo can synthesize nonterminal summaries automatically.

Reusing summaries makes verification nearly twice as fast.

Abstract

Automated verification of all members of a (potentially infinite) set of programs has the potential to be useful in program synthesis, as well as in verification of dynamically loaded code, concurrent code, and language properties. Existing techniques for verification of sets of programs are limited in scope and unable to create or use interpretable or reusable information about sets of programs. The consequence is that one cannot learn anything from one verification problem that can be used in another. Unrealizability Logic (UL), proposed by Kim et al. as the first Hoare-style proof system to prove properties over sets of programs (defined by a regular tree grammar), presents a theoretical framework that can express and use reusable insight. In particular, UL features nonterminal summaries -- inductive facts that characterize recursive nonterminals (analogous to procedure summaries in Hoare logic). In this work, we design the first UL proof synthesis algorithm, implemented as Wuldo. Specifically, we decouple the problem of deciding how to apply UL rules from the problem of synthesizing/checking nonterminal summaries by computing proof structure in a fully syntax-directed fashion. We show that Wuldo, when provided nonterminal summaries, can express and prove verification problems beyond the reach of existing tools, including establishing how infinitely many programs behave on infinitely many inputs. In some cases, Wuldo can even synthesize the necessary nonterminal summaries. Moreover, Wuldo can reuse previously proven nonterminal summaries across verification queries, making verification 1.96 times as fast as when summaries are instead proven from scratch.