OCaml logo
5 Search Results
vocal
VOCaL -- The Verified OCaml Library
Arthur Charguéraud Martin Clochard Jean-Christophe Filliâtre Léon Gondelman Armaël Guéneau Xavier Leroy Cláudio Lourenço Simão Melo de Sousa Andrei Paskevich Mário Pereira François Pottier
0.1
MIT
Used by 0 other packages
why3
Why3 environment for deductive program verification
deductive program verification formal specification automated theorem prover interactive theorem prover
François Bobot Jean-Christophe Filliâtre Claude Marché Guillaume Melquiond Andrei Paskevich
1.5.0
LGPL-2.1-only
Used by 7 other packages
why3-base
Why3 environment for deductive program verification (base)
deductive program verification formal specification automated theorem prover interactive theorem prover
François Bobot Jean-Christophe Filliâtre Claude Marché Guillaume Melquiond Andrei Paskevich
0.88.3
LGPL-2.1-only
Used by 1 other packages
why3-coq
Why3 environment for deductive program verification
deductive program verification formal specification automated theorem prover interactive theorem prover
François Bobot Jean-Christophe Filliâtre Claude Marché Guillaume Melquiond Andrei Paskevich
1.5.0
LGPL-2.1-only
Used by 0 other packages
why3-ide
Why3 environment for deductive program verification
deductive program verification formal specification automated theorem prover interactive theorem prover
François Bobot Jean-Christophe Filliâtre Claude Marché Guillaume Melquiond Andrei Paskevich
1.5.0
LGPL-2.1-only
Used by 0 other packages