|
Entwicklerinformationen
|
libjessie-ocaml-dev | Jessie library for C code analysis | Mehr ... |
Jessie library, from Why certification tool, is useful for deductive verification. It is based on weakest precondition computation techniques and allows to prove that C functions satisfy their specification. |
libwhy-coq | Why library for Coq | Mehr ... |
This package contains all useful logical definitions, lemmas with their proofs and axioms used by Why. Users may need this package when proving some proof obligations in Coq. |
why | A software verification tool | Mehr ... |
Why aims at being a verification conditions generator (VCG) back-end for other verification tools. It provides a powerful input language including higher-order functions, polymorphism, references, arrays and exceptions. It generates proof obligations for many systems: the proof assistants Coq, PVS, Isabelle/HOL, HOL 4, HOL Light, Mizar and the decision procedures Simplify, Alt-Ergo, Yices, CVC Lite and haRVey. |
why-examples | Examples of programs certified with Why | Mehr ... |
Why aims at being a verification conditions generator (VCG) back-end for other verification tools. It provides a powerful input language including higher-order functions, polymorphism, references, arrays and exceptions. It generates proof obligations for many systems: the proof assistants Coq, PVS, Isabelle/HOL, HOL 4, HOL Light, Mizar and the decision procedures Simplify, Alt-Ergo, Yices, CVC Lite and haRVey. . This package contains examples of programs verified using Why. |
|
|
|