Package: why (2.26+dfsg-2+squeeze1)

[ Source: why  ]

A software verification tool

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.

Tags: Software Development: Testing and QA, Implemented in: OCaml, Role: Program

Other Packages Related to why

• dep: libc6 (>= 2.0)

  bibliothèque C GNU embarquée : bibliothèques partagées
  also a virtual package provided by libc6-udeb

• dep: liblablgtk2-ocaml-kc4f2

  virtual package provided by liblablgtk2-ocaml

• dep: make

  outil pour mener la compilation

• dep: ocaml-base-nox-3.11.2

  virtual package provided by ocaml-base-nox

• rec: alt-ergo

  prouveur de théorème automatique dédié à la vérification de programme

• sug: libwhy-coq (= 2.26+dfsg-2+squeeze1)

  Why library for Coq

Download why

Download for all available architectures

Architecture	Package Size	Installed Size	Files
mipsel	14,241.2 kB	37,340.0 kB	[list of files]