package coq-vst-lib

  1. Overview
  2. No Docs
VSTlib: VST-verified C library for VST-verified clients

Install

Dune Dependency

github.com Edit opam file Versions (3)

Authors

  1. A
    Andrew W. Appel
  2. W
    William Mansky

Maintainers

  1. A
    Andrew W. Appel <appel@princeton.edu>

Sources

v2.13.tar.gz
sha512=b51758d5d22f3b67df13203bf33140c828b6df872b710125ed3001ec98da6bc5117ba2843868bbd46c99a9de0ec4cd0d594d61c6b715d9e4daf65f72743a7b63

Description

These program modules, in the form of Verified Software Units, may be linked with client-module code (at the .c/.o level) and proofs (at the .v level).

Tags

date:2023-11-02 keyword:VST keyword:library keyword:malloc keyword:threads keyword:floating-point arithmetic category:Miscellaneous/Coq Extensions category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures logpath:VSTlib

Published: 09 Nov 2023

Dependencies (5)

  1. coq-vst >= "2.11.1" & < "3~"
  2. coq-vcfloat >= "2.1" & < "2.2~"
  3. coq-flocq >= "4.1.0" & < "5.0"
  4. coq-compcert >= "3.11"
  5. coq >= "8.16" & < "8.20~"

Dev Dependencies

None

Used by

None

Conflicts

None