SHF: Small: Usable Verification using Rewriting and Matching Logic

如今，计算机和隐式编程语言被用于许多关键的应用程序中，在这些应用程序中，正确的行为是必要的。因此，为了验证计算系统，必须对所使用的编程语言进行严格的形式化语义定义。不幸的是，尽管在编程语言语义方面的研究已经有40多年了，但大多数程序验证器并不是直接基于形式语义，而是基于其目标编程语言的复杂和特殊的硬件模型。这至少有两个负面后果：首先，它使程序验证器的开发和维护变得困难和不经济，特别是对于新的编程语言或快速发展的语言；其次，它为程序验证器本身的细微错误提供了空间。本研究项目旨在开发一个通用的程序验证框架，该框架将通过其形式语义给出的编程语言作为输入，并产生该语言的程序验证器作为输出。此外，语言语义将是可执行的，因此是可测试的，并且是公开的，因此将作为语言的参考实现和语言理解的正式基础。具体地说，这个项目建立在匹配逻辑及其用于验证可达性属性的最新进展之上。一个独立于语言的健全的、相对完整的证明体系，把一种程序设计语言的操作语义作为一组公理，可以用来推导出该语言中任何程序的任何可达性。这与基于hoare逻辑和动态逻辑的现有验证方法形成鲜明对比，因为这些方法是特定于语言的。因此，这项研究将导致语义和验证技术和算法的发展，这些技术和算法将适用于任何语言，只要给出语言的形式语义。因此，这项研究的更广泛的影响是，它将提高软件系统的质量和健壮性，并将缩小规范和计算机系统实现之间的差距。

Computers, and implicitly programming languages, are used in manycritical applications these days, where correct behavior is necessary.Rigorous, formal semantic definitions of the employed programminglanguages are therefore necessary in order to verify computing systems.Unfortunately, in spite of more than forty years of research inprogramming language semantics, most program verifiers are not directlybased on a formal semantics, but rather on complex and ad-hoc hardwiredmodels of their target programming languages. This has at least twonegative consequences: first, it makes the development and maintenanceof program verifiers hard and uneconomical, particularly for newprogramming languages or languages which evolve fast; second, it allowsroom for subtle bugs in program verifiers themselves. This researchproject aims at developing a generic program verification frameworkthat takes a programming language given through its formal semantics asinput, and yields a program verifier for that language as output.Moreover, the language semantics will be executable, so testable,and public, so will serve as a reference implementation for the languageand as a formal basis for language understanding. Specifically, this projects builds upon recent advances in matching logicand its use for verifying reachability properties. A language-independentsound and relatively complete proof system takes a programming languageoperational semantics as a set of axioms, and can be used to deriveany reachability property about any program in the given language. Thisis in sharp contrast to the existing verification approaches based onHoare logic and on dynamic logic, since these approaches arelanguage-specific. This research will therefore lead to the developmentof semantic and verification techniques and algorithms that will work forany language, provided a formal semantics of the language is given.Consequently, the broader impact of this research is that it will increasethe quality and robustness of software systems, and will narrow the gapbetween the specification and the implementation of computer systems.