nunchaku

A counter-example finder for higher-order logic.
Description

Nunchaku is a counter-example finder for higher-order logic, designed to be used from various proof assistants, and a spiritual successor to Nitpick. It relies encodings and external solvers (CVC4, kodkod, paradox, smbc) to find models, thanks to its modular architecture.

Install
Published
18 Jun 2018
Sources
0.5.1.tar.gz
md5=39f5e6c8b36943062c86b10bb917ea1c
Dependencies
odoc
with-doc
ounit
with-test
qcheck
with-test
qtest
with-test
menhir
build & <= "20181026"
containers
>= "1.0"
jbuilder
>= "1.0+beta7"
ocaml
>= "4.02.0" & < "4.08.0"
Reverse Dependencies