Making Relational Hoare Logic Alignment Complete

TL;DR

This paper proves that a relational Hoare logic can be made alignment complete for a broad class of automata, bridging human reasoning and automata-based automated verification.

Contribution

It establishes a general alignment completeness result for relational Hoare logic using Kleene algebra with tests, solving an open problem.

Findings

Proves alignment completeness for a broad class of automata.

Bridges syntax-based reasoning with automata representations.

Solves an open problem in relational verification.

Abstract

In relational verification, judicious alignment of computational steps facilitates proof of relations between programs using simple relational assertions. Relational Hoare logics (RHL) provide compositional rules that embody various alignments. Seemingly more flexible alignments can be expressed in terms of product automata based on program transition relations. A RHL can be complete, in the ordinary sense, using a single degenerate alignment rule. The notion of alignment completeness was previously proposed as a more satisfactory measure, based on alignment automata, and some rules were shown to be alignment complete with respect to a few ad hoc forms of alignment automata. Using a rule of semantics-preserving rewrites based on Kleene algebra with tests, an RHL is shown to be alignment complete with respect to a very general class of alignment automata. Besides solving the open problem of general alignment completeness, this result bridges between human-friendly syntax-based reasoning and automata representations that facilitate automated verification.