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.

翻译：自动化系统的形式化分析是一个重要且不断发展的领域。该活动通常需要开发新的验证框架以应对新的编程特性或新的考量因素（所关注的缺陷）。其中，一个特定性质往往难以建立：逻辑相对于语义的完备性。本文试图简化此类开发工作，并特别关注完备性问题。为此，我们提出了一个软件分析系统（SAS）的形式化（元）模型，即同名的表示。该模型对被建模的SAS所需假设极少，因此能够涵盖一大类此类系统。随后，我们展示了该方法如何能富有成效地用于理解现有完备性证明的结构，并利用该结构构建新系统并证明其完备性。