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

VST-2.14.tar.gz
sha256=c11551c454057b8a6c7a958534f3ec783e09450ff7e373bfb7c3d6c009d46c06

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:2024-03-20 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: 21 Mar 2024

Dependencies (5)

  1. coq-vst >= "2.13" & < "3~"
  2. coq-vcfloat >= "2.2"
  3. coq-flocq >= "4.1.0" & < "5.0"
  4. coq-compcert >= "3.13"
  5. coq >= "8.17" & < "8.21~"

Dev Dependencies

None

Used by

None

Conflicts

None