package coq-vst-lib
VSTlib: VST-verified C library for VST-verified clients
Install
Dune Dependency
Authors
Maintainers
Sources
v2.15.tar.gz
sha256=44873919ee077b2ce4eb2b7a83c663d3fd673fd7d89c6fc578c46cf10efb4465
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-01-08 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: 08 Jan 2025
Dependencies (5)
-
coq-vst
>= "2.15" -
coq-vcfloat
>= "2.2" -
coq-flocq
>= "4.1.0" & < "5.0" -
coq-compcert
>= "3.15" -
coq
>= "8.19" & < "8.21~"
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page