表示法 (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 modeled, 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仅需少量假设，因此能够捕捉一大类此类系统。随后，我们展示了我们的方法如何能够富有成效，既可用于理解现有完备性证明的结构方式，也可利用该结构构建新系统并证明其完备性。