package coq-vst

  1. Overview
  2. No Docs
Verified Software Toolchain

Install

Dune Dependency

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

Authors

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

Maintainers

  1. V
    VST team

Sources

VST-3.0beta2.tar.gz
sha256=3050363f1e956adf08355dd5f6439de8ebc519d4e518d0866abceb948c4a4d82

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:2024-04-12

Published: 15 Apr 2024

Dependencies (6)

  1. coq-iris = "4.2.0"
  2. coq-flocq >= "4.1.0"
  3. coq-vst-zlist = "2.13"
  4. coq-compcert = "3.13.1"
  5. coq >= "8.18" & < "8.20~"
  6. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None