(Copyright (C) 2011-2013 Carlo A. Furia)

QFIS is a verifier for the theory of quantifier-free integer sequences.


This directory contains:

  • src/ Eiffel source files of the verifier
  • bin/ compiled binaries (moved there by the installation script)
  • examples/ Examples of programs verifiable with qfis
  • qfis.ecf EiffelStudio compiler configuration file
  • build-linux.sh Bash script to compile under Linux
  • README.md this file
  • COPYING the distribution license (GNU GPL v3)


To compile:

  • install the Eiffel Studio compiler (command ec should be reachable in the path)
  • run the compilation script for your system (you may have to adjust the references in qfis.ecf)

To install QFIS move (or copy) the executable for your system into a directory reachable from the path.

This distribution of QFIS has been compiled and tested with EiffelStudio 7.0 and CVC3 2.2.

Using QFIS

Running qfis -h gives a summary of basic usage and the command-line options.

QFIS relies on CVC3 as back-end to solve verification condition. See http://www.cs.nyu.edu/acsys/cvc3/ for instructions on how to obtain CVC3.

You can obtain a user manual for QFIS (also including more detailed installation instructions) from http://bugcounting.net/publications.html#qfis-manual.

You can also try out QFIS online on COMCOM or watch a video demo (make sure to select HD and go full-screen for best readability).