Bug#415862: ITP: why -- A software verification tool

[Samuel Mimram <smimram@debian.org>]

Package: wnpp
Severity: wishlist
Owner: Samuel Mimram <smimram@debian.org>

* Package name    : why
  Version         : 2.02
  Upstream Author : Jean-Christophe Filliâtre
* URL             : http://why.lri.fr/
* License         : GPL
  Programming Lang: OCaml
  Description     : 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, Ergo, Yices, CVC Lite and haRVey.

-- System Information:
Debian Release: 4.0
  APT prefers unstable
  APT policy: (500, 'unstable'), (500, 'testing'), (1, 'experimental')
Architecture: amd64 (x86_64)
Shell:  /bin/sh linked to /bin/bash
Kernel: Linux 2.6.18-4-amd64
Locale: LANG=en_US.UTF-8, LC_CTYPE=en_US.UTF-8 (charmap=UTF-8) (ignored: LC_ALL set to en_US.UTF-8)