Last updated: 2016-05-18 21:22:55 +0100

Upstream URL: git clone http://chriswarbo.net/git/tip-benchmarks.git


View repository

View issue tracker

Contents of follows

TIP: Tons of Inductive Problems

This repository contains benchmarks and challenge problems for inductive theorem provers. The benchmarks are written in a superset of SMTLIB under the benchmarks/ directory and its subdirectories. Each file contains exactly one problem.

The original directory contains the original Haskell source files for many of the problems.

The benchmarks are also available to download in Why3 format, and a CVC4-compatible version of SMTLIB:

Generating problems yourself

After installing the TIP tools you can generate the whole problem set in TIP, Why3 and CVC4 format yourself from the Haskell sources. To do this run omake. This may be useful if you want to add your own problems, but it is not a requirement that they come from a Haskell source file.

Contributing to the TIP benchmarks

Contributions are most encouraged! Any inductive problem, big or small, simple or difficult is welcome.

The simplest method to add new benchmarks is via a github pull request to this git repo.

We're also looking for non-theorem benchmarks to evaluate tools that find counterexamples to false properties. They can be expressed in the same format, but should be under another directory, to be able to keep them apart.

You are also free to email the maintainers with new problems (or questions):