Skip navigation
Please use this identifier to cite or link to this item: http://arks.princeton.edu/ark:/88435/dsp0137720c91t
 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 URI: http://arks.princeton.edu/ark:/88435/dsp0137720c91t Type of Material: Princeton University Senior Theses Language: en_US Appears in Collections: Computer Science, 1988-2016

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

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