Representations
Paul Brunet
TL;DR
Representations provides a modular meta-model for formal software analysis systems by combining category-theoretic and relation-algebraic methods. The core idea is to treat SAS as representations $R=\langle T,E,\models,\leq\rangle$, form a cartesian category of representations $\mathbf{Repr}$ with morphisms and products, and use reductions to transfer completeness results between representations. The paper extends the framework to higher-order, set-indexed representations (HORs), enabling parametric, multi-tier analyses and showing how HOR lifting yields flexible, modular models that can capture Kleene-algebra extensions (KA, KAT, SKA, CKA). Together, these tools aim to enable systematic, transparent construction of sound and complete SAS and to integrate with related specification theories and institutional frameworks. The work outlines future directions for tooling, classification of representation classes, and deeper meta-theory for abstract verification frameworks.
Abstract
The formal analysis of automated systems is an important and growing industry. This activity routinely requires new verification frameworks to be developed to tackle new programming features, or new considerations (bugs of interest). Often, one particular property can prove frustrating to establish: completeness of the logic with respect to the semantics. In this paper, we try and make such developments easier, with a particular attention on completeness. Towards that aim, we propose a formal (meta-)model of software analysis systems (SAS), the eponymous Representations. This model requires few assumptions on the SAS being modelled, and as such is able to capture a large class of such systems. We then show how our approach can be fruitful, both to understand how existing completeness proofs can be structured, and to leverage this structure to build new systems and prove their completeness.