dogear

enter for all results · esc to close

VST

vst.cs.princeton.edusite

Toolchain for verifying C code inside Coq in a higher-order concurrent, impredicative separation logic that is sound w.r.t. the Clight language of the CompCert compiler.

visit vst.cs.princeton.edu ↗
0
sign in to dogear this
from
Coq
added
2026-10-10
likes
0

similar

  1. CertiCoq github.com
    tool category #coq link ↗

    Verified compiler from Gallina, the internal language of Coq, down to CompCert's Clight language.

  2. Volume 5: Verifiable C softwarefoundations.cis.upenn.edu
    site category #coq link ↗

    An extended tutorial on specifying and verifying C programs using the Verified Software Toolchain.

  3. Program Logics for Certified Compilers cs.princeton.edu
    site category #coq link ↗

    Book that explains how to construct program logics using separation logic, accompanied by a formal model in Coq which is applied to the Clight programming language and other examples.

  4. VsCoq github.com
    tool category #coq link ↗

    Language server and extension for the Visual Studio Code and VSCodium editors.

  5. SMTCoq github.com
    tool category #coq link ↗

    Tool that checks proof witnesses coming from external SAT and SMT solvers.

  6. Coq LSP github.com
    tool category #coq link ↗

    Language server and extension for the Visual Studio Code and VSCodium editors with custom document checking engine.

Coq › Projects > Frameworks: “Toolchain for verifying C code inside Coq in a higher-order concurrent, impredicative separation logic that is sound w.r.t. the Clight language of the CompCert compiler.”