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 journalArticlepeer-review

16 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 languageEnglish (US)
Pages (from-to)367-422
Number of pages56
JournalJournal of Automated Reasoning
Volume61
Issue number1-4
DOIs
StatePublished - Jun 1 2018

All Science Journal Classification (ASJC) codes

  • Software
  • Computational Theory and Mathematics
  • Artificial Intelligence

Keywords

  • Program verification
  • Proof automation
  • Separation logic
  • Symbolic execution

Fingerprint Dive into the research topics of 'VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs'. Together they form a unique fingerprint.

Cite this