package coq-vst-lib

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

Install

Dune Dependency

Authors

Maintainers

Sources

lib-2.15.1.tar.gz
sha256=b08762b1b250e3e351e179fbf82c8618148f3160c545daab9e3b2103cf9e0d4e

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).

Dependencies (5)

  1. coq-vst >= "2.15"
  2. coq-vcfloat >= "2.3"
  3. coq-flocq >= "4.1.0" & < "5.0"
  4. coq-compcert >= "3.15"
  5. coq >= "8.19" & < "8.21~"

Dev Dependencies

None

Used by

None

Conflicts

None

Rocq

Interactive Theorem Prover