A Program Logic for Abstract (Hyper)Properties

TL;DR

APPL offers a unified Hoare-style program logic parameterised by an abstract domain, unifying correctness, incorrectness, and hyperproperty reasoning within a single semantic framework built from a complete lattice, a join-basis, and an infinitary monoidal operator $\oplus$. The core insight is that the assertion language is itself a semantic abstraction, enabling best-correct-approximation derivations and relative completeness when sufficient expressivity is present. By instantiating APPL’s parameters, classical Hoare logic, interval Hoare logic, incorrectness logic, and Hyper Hoare Logic are recovered as concrete instances, while abstract logics APPL$_A$ and hyperproperty abstractions extend reasoning to abstract and hyperdomains. The framework also analyzes abstraction of hyperproperties via down-closed, pointwise, and interval-based constructions, showing soundness and completeness results under suitable algebraic conditions. Overall, APPL provides a principled, algebraic foundation for designing and combining abstractions in hyperproperty verification and static analysis.

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.

Figures (8)

• Figure 1: The program logic $\text{APPL}$ over the interpretation monoid $(D, \sqsubseteq, \oplus, \operatorname{B})$.
• Figure 2: Derivation for Example \ref{['ex:intervals-logic']}
• Figure 3: Derivation for Example \ref{['ex:incorr-LCL-example']}
• Figure 4: Derivation for Example \ref{['ex:hyper-muller']}
• Figure 5: The abstract program logic $\text{APPL}_{A}$: some key rules, where $\llbracket{\mathsf{e}} \rrbracket^A a$ abbreviates $\bigsqcup^A \{ \llparenthesis \mathsf{e} \rrparenthesis^A b \in A \mid {b \in \alpha(\operatorname{B})},\, \alpha(b) \sqsubseteq_A a\}$.

Theorems & Definitions (34)

• definition 1: Dense subset
• definition 2: Weight wrt a Basis
• definition 3: $\kappa$-Quantale
• definition 4: Commands
• definition 5: Interpretation monoid
• proof
• definition 6: Basis and Full Semantics
• proof
• proof
• definition 7: Additive combination of a family of functions