Using Reflective Separation-Entailment Solvers for Reasoning Formally About C: Integrating the Verified Software Toolchain with the MirrorShard Solver

Abstract

Formal software verification is a growing field of research in computer science. The aim of software verifciation research is to create technologies for reasoning formally about software, and to use such technologies to prove interesting and useful results. By proving programs correct, with respect to particular specifications of what correctness means for the programs in question, we can derive much stronger guarantees about how the software will behave when run than would be possible through other means, such as testing. In this paper we discuss improvements we have made to the Verified Software Toolchain (VST), a system for formal reasoning about C programs, and we distill lessons from this project that might be more widely applicable to similar projects in the future. In particular, we describe the process of integrating VST with MirrorShard, a reflective solver for expressions in separation logic. Separation logic is used internally by VST to express properties of programs that relate to their usage of heap memory. After this discussion, we reflect on the future work that remains to be done in VST, and on how the work described in this paper can be built upon to further increase VST's power and usability, as well as possibly serving as an example for other projects.