SHF: Small: Usable Verification using Rewriting and Matching Logic

SHF：小：使用重写和匹配逻辑进行可用验证

• 批准号: 1218605
• 负责人: Grigore Rosu
• 金额: $ 40万
• 依托单位: University of Illinois at Urbana-Champaign
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2012
• 资助国家: 美国
• 起止时间: 2012-08-15 至 2015-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1218605&HistoricalAwards=false
• 关键词: SHF; Small; Usable; Verification; using

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.

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