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

lib-2.12.tar.gz
sha256=90a021b7f8175d264ddc1633d267a2543514549de574f5e09aa5e0524a26864e

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-04-14 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: 15 Apr 2023

Dependencies (5)

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

Dev Dependencies

None

Used by

None

Conflicts

None