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

Qinxiang Cao; Lennart Beringer; Samuel Gruetter; Josiah Dodds; Andrew W. Appel

doi:10.1007/s10817-018-9457-5

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

Qinxiang Cao, Lennart Beringer, Samuel Gruetter, Josiah Dodds, Andrew W. Appel

Research output: Contribution to journal › Article › peer-review

66 Scopus citations

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.

Original language	English (US)
Pages (from-to)	367-422
Number of pages	56
Journal	Journal of Automated Reasoning
Volume	61
Issue number	1-4
DOIs	https://doi.org/10.1007/s10817-018-9457-5
State	Published - Jun 1 2018
Externally published	Yes

All Science Journal Classification (ASJC) codes

Software
Computational Theory and Mathematics
Artificial Intelligence

Keywords

Program verification
Proof automation
Separation logic
Symbolic execution

Access to Document

10.1007/s10817-018-9457-5

Cite this

@article{6fb426dafcf142f8938738949b1d8388,

title = "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 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 = "Program verification, Proof automation, Separation logic, Symbolic execution",

author = "Qinxiang Cao and Lennart Beringer and Samuel Gruetter and Josiah Dodds and Appel, {Andrew W.}",

note = "Publisher Copyright: {\textcopyright} 2018, Springer Science+Business Media B.V., part of Springer Nature.",

year = "2018",

month = jun,

day = "1",

doi = "10.1007/s10817-018-9457-5",

language = "English (US)",

volume = "61",

pages = "367--422",

journal = "Journal of Automated Reasoning",

issn = "0168-7433",

publisher = "Springer Netherlands",

number = "1-4",

}

TY - JOUR

T1 - VST-Floyd

T2 - A Separation Logic Tool to Verify Correctness of C Programs

AU - Cao, Qinxiang

AU - Beringer, Lennart

AU - Gruetter, Samuel

AU - Dodds, Josiah

AU - Appel, Andrew W.

PY - 2018/6/1

Y1 - 2018/6/1

N2 - 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.

AB - 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.

KW - Program verification

KW - Proof automation

KW - Separation logic

KW - Symbolic execution

UR - http://www.scopus.com/inward/record.url?scp=85042219085&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85042219085&partnerID=8YFLogxK

U2 - 10.1007/s10817-018-9457-5

DO - 10.1007/s10817-018-9457-5

M3 - Article

AN - SCOPUS:85042219085

SN - 0168-7433

VL - 61

SP - 367

EP - 422

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

IS - 1-4

ER -

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

Abstract

All Science Journal Classification (ASJC) codes

Keywords

Access to Document

Other files and links

Fingerprint

Cite this