package coq-vst-lib
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).
Tags
date:2025-02-10 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:VSTlibPublished: 10 Feb 2025
Dependencies (5)
-
coq-vst
>= "2.15"
-
coq-vcfloat
>= "2.3"
-
coq-flocq
>= "4.1.0" & < "5.0"
-
coq-compcert
>= "3.15"
-
coq
>= "8.19" & < "8.21~"
Dev Dependencies
None
Used by
None
Conflicts
None
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page