Concise Outlines for a Complex Logic: A Proof Outline Checker for TaDA (Full Paper)

TL;DR

This paper introduces a proof outline checker for the TaDA logic, enabling automated validation of complex program proofs with greater simplicity and automation than traditional interactive or fully automatic methods.

Contribution

It systematically develops a proof outline checker for TaDA, simplifying proof validation and enhancing automation compared to existing interactive and automatic verifiers.

Findings

The checker automates proof validation for TaDA logic.

It reduces complex proof checking to simpler, existing verification problems.

The approach balances automation and simplicity, facilitating experimentation with program logics.

Abstract

Modern separation logics allow one to prove rich properties of intricate code, e.g. functional correctness and linearizability of non-blocking concurrent code. However, this expressiveness leads to a complexity that makes these logics difficult to apply. Manual proofs or proofs in interactive theorem provers consist of a large number of steps, often with subtle side conditions. On the other hand, automation with dedicated verifiers typically requires sophisticated proof search algorithms that are specific to the given program logic, resulting in limited tool support that makes it difficult to experiment with program logics, e.g. when learning, improving, or comparing them. Proof outline checkers fill this gap. Their input is a program annotated with the most essential proof steps, just like the proof outlines typically presented in papers. The tool then checks automatically that this outline represents a valid proof in the program logic. In this paper, we systematically develop a proof outline checker for the TaDA logic, which reduces the checking to a simpler verification problem, for which automated tools exist. Our approach leads to proof outline checkers that provide substantially more automation than interactive provers, but are much simpler to develop than custom automatic verifiers.