VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs
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 se...
| Main Authors: | , , , , |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | English |
| Published: |
Springer Netherlands
2021
|
| Online Access: | https://hdl.handle.net/1721.1/131755 |
| _version_ | 1826195325935681536 |
|---|---|
| author | Cao, Qinxiang Beringer, Lennart Gruetter, Samuel Dodds, Josiah Appel, Andrew W |
| author2 | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory |
| author_facet | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Cao, Qinxiang Beringer, Lennart Gruetter, Samuel Dodds, Josiah Appel, Andrew W |
| author_sort | Cao, Qinxiang |
| collection | MIT |
| 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. |
| first_indexed | 2024-09-23T10:10:52Z |
| format | Article |
| id | mit-1721.1/131755 |
| institution | Massachusetts Institute of Technology |
| language | English |
| last_indexed | 2024-09-23T10:10:52Z |
| publishDate | 2021 |
| publisher | Springer Netherlands |
| record_format | dspace |
| spelling | mit-1721.1/1317552023-12-22T19:22:17Z VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs Cao, Qinxiang Beringer, Lennart Gruetter, Samuel Dodds, Josiah Appel, Andrew W Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory 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. 2021-09-20T17:30:09Z 2021-09-20T17:30:09Z 2018-02-21 2020-09-24T20:35:45Z Article http://purl.org/eprint/type/JournalArticle https://hdl.handle.net/1721.1/131755 en https://doi.org/10.1007/s10817-018-9457-5 Article is made available in accordance with the publisher's policy and may be subject to US copyright law. Please refer to the publisher's site for terms of use. Springer Science+Business Media B.V., part of Springer Nature application/pdf Springer Netherlands Springer Netherlands |
| spellingShingle | Cao, Qinxiang Beringer, Lennart Gruetter, Samuel Dodds, Josiah Appel, Andrew W VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs |
| title | VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs |
| title_full | VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs |
| title_fullStr | VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs |
| title_full_unstemmed | VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs |
| title_short | VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs |
| title_sort | vst floyd a separation logic tool to verify correctness of c programs |
| url | https://hdl.handle.net/1721.1/131755 |
| work_keys_str_mv | AT caoqinxiang vstfloydaseparationlogictooltoverifycorrectnessofcprograms AT beringerlennart vstfloydaseparationlogictooltoverifycorrectnessofcprograms AT gruettersamuel vstfloydaseparationlogictooltoverifycorrectnessofcprograms AT doddsjosiah vstfloydaseparationlogictooltoverifycorrectnessofcprograms AT appelandreww vstfloydaseparationlogictooltoverifycorrectnessofcprograms |