表示法 (Representations)

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要求极少假设，因此能够捕获此类系统的广泛类别。随后，我们展示了该方法如何富有成效：既可用于理解现有完备性证明的结构，也可利用该结构构建新系统并证明其完备性。