Please use this identifier to cite or link to this item: http://arks.princeton.edu/ark:/88435/dsp010r9676504
DC FieldValueLanguage
dc.contributor.authorCao, Qinxiang-
dc.contributor.otherComputer Science Department-
dc.date.accessioned2018-10-09T21:11:43Z-
dc.date.available2018-10-09T21:11:43Z-
dc.date.issued2018-
dc.identifier.urihttp://arks.princeton.edu/ark:/88435/dsp010r9676504-
dc.description.abstractIn our interconnected world, software bugs can seriously compromise our safety and security. To provide adequate safety or protection, security-critical kernels (of large systems) must be functionally correct. To ensure functional correctness of C programs, we can use Hoare logic and its extensions such as separation logic. But such correctness proofs are large and complex enough that we cannot trust them unless they are machine-checked. This dissertation shows how we can construct machine-checked proofs of program correctness using separation logic. I answer three questions: How shall we specify our programs? How shall we prove our programs correct with respect to their specifications? How shall we mechanize such correctness proofs? I present practical techniques for separation-logic-based program verification and demonstrate them on several examples. I introduce VST-Floyd, a tool for users to build formal C program correctness proofs in Coq using separation logic. VST-Floyd is built based on Verifiable C, a proved sound separation logic; I show how to reformulate its rules to make them practical for use in verification.-
dc.language.isoen-
dc.publisherPrinceton, NJ : Princeton University-
dc.relation.isformatofThe Mudd Manuscript Library retains one bound copy of each dissertation. Search for these copies in the library's main catalog: <a href=http://catalog.princeton.edu> catalog.princeton.edu </a>-
dc.subjectHoare logic-
dc.subjectinteractive theorem proving-
dc.subjectprogram verification-
dc.subjectSeparation logic-
dc.subject.classificationComputer science-
dc.titleSeparation-Logic-Based Program Verification in Coq-