SHF: Small: Usable Verification using Rewriting and Matching Logic

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

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.