SHF: Small: Usable Verification using Rewriting and Matching Logic

点击翻译按钮获取中文摘要

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.