A Program Logic for Abstract (Hyper)Properties

TL;DR

The paper introduces APPL, a unifying logic framework for abstract and hyperproperties, grounded in a semantic lattice-based approach with flexible nondeterministic choice interpretation.

Contribution

It presents a new, flexible program logic that unifies existing logics and extends to novel abstractions of properties and hyperproperties.

Findings

APPL subsumes standard Hoare, incorrectness, and Hyper Hoare logics.

The logic is sound and relatively complete with expressive property languages.

It provides a sound abstract deduction system based on best correct approximations.

Abstract

We introduce APPL (Abstract Program Property Logic), a unifying Hoare-style logic that subsumes standard Hoare logic, incorrectness logic, and several variants of Hyper Hoare logic. APPL provides a principled foundation for abstract program logics parameterised by an abstract domain, encompassing both existing and novel abstractions of properties and hyperproperties. The logic is grounded in a semantic framework where the meaning of commands is first defined on a lattice basis and then extended to the full lattice via additivity. Crucially, nondeterministic choice is interpreted by a monoidal operator that need not be idempotent nor coincide with the lattice join. This flexibility allows the framework to capture collecting semantics, various classes of abstract semantics, and hypersemantics. The APPL proof system is sound, and it is relatively complete whenever the property language is sufficiently expressive. When the property language is restricted to an abstract domain, the result is a sound abstract deduction system based on best correct approximations. Relative completeness with respect to a corresponding abstract semantics is recovered provided the abstract domain is complete, in the sense of abstract interpretation, for the monoidal operator.