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