Section: New Software and Platforms

The Nunchaku Higher-Order Model Finder

Functional Description

Nunchaku is a model finder for higher-order logic, with dedicated support for various definitional principles. It is designed to work as a backend for various proof assistants and to use state-of-the-art model finders and other solvers as backends.

In 2016, the first three versions of the tools were released (0.1 through 0.3). The Isabelle2016-1 release includes Nunchaku as well as the frontend that bridges the gap between the proof assistant and the model finder. Work has commenced on a Coq frontend [28] and a TLA⁺ frontend. Currently, the backends CVC4, Kodkod, and Paradox are supported.

• Participants: Jasmin Blanchette and Simon Cruanes

• Contact: Jasmin Blanchette

• URL: https://github.com/nunchaku-inria