Skip navigation
Please use this identifier to cite or link to this item:
Title: Using Reflective Separation-Entailment Solvers for Reasoning Formally About C: Integrating the Verified Software Toolchain with the MirrorShard Solver
Authors: Alvarez, Mario
Advisors: Appel, Andrew
Department: Computer Science
Class Year: 2014
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.
Extent: 41 pages
Type of Material: Princeton University Senior Theses
Language: en_US
Appears in Collections:Computer Science, 1988-2020

Files in This Item:
File SizeFormat 
alvarez_mario_thesis_final.pdf615.14 kBAdobe PDF    Request a copy

Items in Dataspace are protected by copyright, with all rights reserved, unless otherwise indicated.