package coq-vst-64

  1. Overview
  2. No Docs
Verified Software Toolchain

Install

Dune Dependency

vst.cs.princeton.edu Edit opam file Versions (1)

Authors

  1. A
    Andrew W. Appel
  2. L
    Lennart Beringer
  3. S
    Sandrine Blazy
  4. Q
    Qinxiang Cao
  5. S
    Santiago Cuellar
  6. R
    Robert Dockins
  7. J
    Josiah Dodds
  8. N
    Nick Giannarakis
  9. S
    Samuel Gruetter
  10. A
    Aquinas Hobor
  11. J
    Jean-Marie Madiot
  12. W
    William Mansky

Maintainers

  1. V
    VST team

Sources

v2.6.tar.gz
sha512=4fea46c423fd5abfa403ae88bc34a859960c6e7bbafddc1f208fc4d93af29b0711804a5eb3c917cd70d407f9a3deffa7157edc4bbfef186635280080153f47b3

Description

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.

Tags

category:Computer Science/Semantics and Compilation/Semantics keyword:C logpath:VST date:2020-08-02

Published: 03 Aug 2020

Dependencies (4)

  1. coq-flocq >= "3.2.1"
  2. coq-compcert-64 (= "3.7~coq-platform~open-source") | (= "3.7~coq-platform") | (= "3.7+8.12~coq_platform~open_source") | (= "3.7+8.12~coq_platform")
  3. coq >= "8.11" & < "8.13"
  4. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None