Skip to main content

VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs

Author(s): Cao, Qinxiang; Beringer, Lennart; Gruetter, Samuel; Dodds, Josiah; Appel, Andrew W

To refer to this page use:
Abstract: The Verified Software Toolchain builds foundational machine-checked proofs of the functional correctness of C programs. Its program logic, Verifiable C, is a shallowly embedded higher-order separation Hoare logic which is proved sound in Coq with respect to the operational semantics of CompCert Clight. This paper introduces VST-Floyd, a verification assistant which offers a set of semiautomatic tactics helping users build functional correctness proofs for C programs using Verifiable C.
Publication Date: 21-Feb-2018
Citation: Cao, Qinxiang, Lennart Beringer, Samuel Gruetter, Josiah Dodds, and Andrew W. Appel. "VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs." Journal of Automated Reasoning 61, no. 1 (2018): 367-422. doi:10.1007/s10817-018-9457-5
DOI: doi:10.1007/s10817-018-9457-5
ISSN: 0168-7433
EISSN: 1573-0670
Pages: 367 - 422
Type of Material: Journal Article
Journal/Proceeding Title: Journal of Automated Reasoning
Version: Author's manuscript

Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.