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
DownloadTo refer to this page use:
http://arks.princeton.edu/ark:/88435/pr1tf9nFull metadata record
| DC Field | Value | Language |
|---|---|---|
| dc.contributor.author | Cao, Qinxiang | - |
| dc.contributor.author | Beringer, Lennart | - |
| dc.contributor.author | Gruetter, Samuel | - |
| dc.contributor.author | Dodds, Josiah | - |
| dc.contributor.author | Appel, Andrew W | - |
| dc.date.accessioned | 2021-10-08T19:44:32Z | - |
| dc.date.available | 2021-10-08T19:44:32Z | - |
| dc.date.issued | 2018-02-21 | en_US |
| dc.identifier.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 | en_US |
| dc.identifier.issn | 0168-7433 | - |
| dc.identifier.uri | https://www.cs.princeton.edu/~appel/papers/VST-Floyd.pdf | - |
| dc.identifier.uri | http://arks.princeton.edu/ark:/88435/pr1tf9n | - |
| dc.description.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. | en_US |
| dc.format.extent | 367 - 422 | en_US |
| dc.language.iso | en_US | en_US |
| dc.relation.ispartof | Journal of Automated Reasoning | en_US |
| dc.rights | Author's manuscript | en_US |
| dc.title | VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs | en_US |
| dc.type | Journal Article | en_US |
| dc.identifier.doi | doi:10.1007/s10817-018-9457-5 | - |
| dc.identifier.eissn | 1573-0670 | - |
| pu.type.symplectic | http://www.symplectic.co.uk/publications/atom-terms/1.0/journal-article | en_US |
Files in This Item:
| File | Description | Size | Format | |
|---|---|---|---|---|
| ToolVerifyCorrectCPrograms.pdf | 547.9 kB | Adobe PDF | View/Download |
Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.