Institute for Computer Languages
Compilers and Languages Group

Vinter: A Vampire-Based Tool for Interpolation

Vinter is a Vampire-based tool for interpolation, whose aim is to generate minimal interpolants.

Vinter translates arbitraty proofs into interpolating ones (local proofs), extracts interpolants from local proofs, and minimises interpolants using various measures, such as for example the size of the interpolants or the number of quantifiers used in the interpolants.

Vinter takes an input problem written in either SMT-LIB or TPTP syntax. Proofs are found using either Z3 or Vampire, solving pseudo-boolean optimisation is delegated to Yices, while localising proofs and generating minimal interpolants is done by Vampire.

Source Code

The latest release of Vinter is: vinter-2012-02-01.tar.gz

Note: To run Vinter, you also need to have the Z3 and Yices executables.

Benchmarks

See the examples to try Vinter.

Publications

Vinter is based on the technique of playing in the grey area of proofs to find interpolants minimal with respect to various measures.

Complang
Laura Kovács
   ARV
   ATCS
   Student-Projects
   Vinter
   Cade-Vampire-Tutorial
   SYNASC-Tutorial
   CATPVS
Sitemap
Faculty of Informatics
Vienna University of Technology
top | HTML 4.01 | last update: 2015-02-20 (Webmaster)