Automating Unrealizability Logic: Hoare-style Proof Synthesis for Infinite Sets of Programs
CoRR(2024)
摘要
Unrealizability logic (UL) was proposed by Kim et al. as the first
Hoare-style proof system for proving properties that hold for an infinite set
of programs (defined by a regular tree grammar). The goal of our work is to
automate reasoning and proof generation for UL. A key ingredient in UL is the
notion of nonterminal summaries-inductive facts that characterize recursive
nonterminals in the grammar that defines the set of programs. They are
analogous to procedure summaries in Hoare logic. The goal of automating UL led
us to reformulate the inference rules-in particular, introducing a unified rule
for nonterminal summaries, called the rule of adaptation, which draws
inspiration from how procedure summaries are handled in Hoare logic. In the
same way that verification conditions can be used to synthesize loop invariants
for Hoare logic proofs, our reformulation of UL reduces the problem of
synthesizing a nonterminal summary to a Syntax-Guided Synthesis problem. We
implement Wuldo, the first checker and synthesizer for UL. Wuldo can express
proofs beyond the reach of existing tools, including proofs that establish how
infinitely many programs behave on infinitely many inputs, and in some cases
Wuldo can even synthesize the needed nonterminal summaries.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要