coq-vst

Verified Software Toolchain The software toolchain includes static analyzers to check assertions about your program; optimizing compilers to translate your program to machine language; operating systems and libraries to supply context for your program. The Verified Software Toolchain project assures with machine-checked proofs that the assertions claimed at the top of the toolchain really hold in the machine-language program, running in the operating-system context.

opam install coq-vst.2.2
homepage
http://vst.cs.princeton.edu/
license
https://raw.githubusercontent.com/PrincetonUniversity/VST/master/LICENSE
bugs tracker
https://github.com/PrincetonUniversity/VST/issues
dependencies
coq >= 8.7.0 & coq-compcert = 3.3.0
source
https://github.com/PrincetonUniversity/VST/archive/v2.2.tar.gz
package
https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-vst/coq-vst.2.2