VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs |
| |
| Authors: | Qinxiang Cao Lennart Beringer Samuel Gruetter Josiah Dodds Andrew W Appel |
| |
| Affiliation: | 1.Department of Computer Science,Princeton University,Princeton,USA;2.Department of EECS,MIT,Cambridge,USA;3.Galois, Inc.,Portland,USA |
| |
| 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. |
| |
| Keywords: | |
| 本文献已被 SpringerLink 等数据库收录！ |
|
