package coq-vst-32

  1. Overview
  2. No Docs
Verified Software Toolchain

Install

Dune Dependency

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

Authors

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

Maintainers

  1. V
    VST team

Sources

v2.11.1.tar.gz
sha512=9d66a1a0f428199110d89a8b4e90d50ad9b6448c92b5ad0859a1bcae9bf1153ea016b5af1ab9f4dc441b5af307968445f4b134cdb80593a6e9a974be94cc5730

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:2022-08-19

Published: 13 Dec 2022

Dependencies (5)

  1. coq-flocq >= "4.1.0"
  2. coq-vst-zlist = "2.11"
  3. coq-compcert-32 = "3.11"
  4. coq >= "8.14" & < "8.17~"
  5. ocaml

Dev Dependencies

None

Used by

None

Conflicts (1)

  1. coq-vst