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 |
| Summary: | 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. |
|---|