Volume 5: Verifiable C

softwarefoundations.cis.upenn.edusite

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

from

Coq

added

2026-10-10

likes

0

similar

1. ▲
   Volume 3: Verified Functional Algorithms softwarefoundations.cis.upenn.edu

   site category #coq link ↗

   Demonstration of how a variety of fundamental data structures can be specified and verified.

2. ▲
   VST vst.cs.princeton.edu

   site category #coq link ↗

   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.

3. ▲
   VCFloat github.com

   tool category #coq link ↗

   Framework for verifying C programs with floating-point computations.

   
4. ▲
   CertiCoq github.com

   tool category #coq link ↗

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

5. ▲
   Proofs and Reliable Programming using Coq team.inria.fr

   site category #coq link ↗

   Introduction to developing and verifying programs with Coq.

6. ▲
   JSCert github.com

   tool category #coq link ↗

   Coq specification of ECMAScript 5 (JavaScript) with verified reference interpreter.

   

Coq › Resources > Books: “An extended tutorial on specifying and verifying C programs using the Verified Software Toolchain.”