SHF: Small: Usable Verification using Rewriting and Matching Logic

University Of Illinois At Urbana-Champaign, Urbana IL

Investigators

Abstract

Computers, and implicitly programming languages, are used in many critical applications these days, where correct behavior is necessary. Rigorous, formal semantic definitions of the employed programming languages are therefore necessary in order to verify computing systems. Unfortunately, in spite of more than forty years of research in programming language semantics, most program verifiers are not directly based on a formal semantics, but rather on complex and ad-hoc hardwired models of their target programming languages. This has at least two negative consequences: first, it makes the development and maintenance of program verifiers hard and uneconomical, particularly for new programming languages or languages which evolve fast; second, it allows room for subtle bugs in program verifiers themselves. This research project aims at developing a generic program verification framework that takes a programming language given through its formal semantics as input, 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 language and as a formal basis for language understanding. Specifically, this projects builds upon recent advances in matching logic and its use for verifying reachability properties. A language-independent sound and relatively complete proof system takes a programming language operational semantics as a set of axioms, and can be used to derive any reachability property about any program in the given language. This is in sharp contrast to the existing verification approaches based on Hoare logic and on dynamic logic, since these approaches are language-specific. This research will therefore lead to the development of semantic and verification techniques and algorithms that will work for any language, provided a formal semantics of the language is given. Consequently, the broader impact of this research is that it will increase the quality and robustness of software systems, and will narrow the gap between the specification and the implementation of computer systems.