devel/why3 - The NetBSD Packages Collection

Platform for deductive program verification

Why3 is a platform for deductive program verification. It provides a rich
language for specification and programming, called WhyML, and relies
on external theorem provers, both automated and interactive, to
discharge verification conditions.

Why3 comes with a standard library of logical theories (integer and
real arithmetic, Boolean operations, sets and maps, etc.) and basic
programming data structures (arrays, queues, hash tables, etc.). A
user can write WhyML programs directly and get correct-by-construction
OCaml programs through an automated extraction mechanism. WhyML is
also used as an intermediate language for the verification of C, Java,
or Ada programs.

Build dependencies

pkgtools/mktools devel/gmake pkgtools/cwrappers

Runtime dependencies

devel/menhir lang/coq lang/ocaml devel/ocamlgraph math/ocaml-num devel/ocamlgraph math/ocaml-num

Binary packages

NetBSD 10.0_BETAx86_64why3-1.5.1nb1.tgz
NetBSD 9.0i386why3-1.5.1nb1.tgz
NetBSD 9.0x86_64why3-1.5.1nb1.tgz
NetBSD 9.3x86_64why3-1.5.1nb1.tgz

Binary packages can be installed with the high-level tool pkgin (which can be installed with pkg_add) or pkg_add(1) (installed by default). The NetBSD packages collection is also designed to permit easy installation from source.

Available build options


Known vulnerabilities

The pkg_admin audit command locates any installed package which has been mentioned in security advisories as having vulnerabilities.

Please note the vulnerabilities database might not be fully accurate, and not every bug is exploitable with every configuration.

Problem reports, updates or suggestions for this package should be reported with send-pr.