(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.ecfEiffelStudio compiler configuration file
build-linux.shBash script to compile under Linux
COPYINGthe distribution license (GNU GPL v3)
- install the Eiffel Studio compiler (command
ecshould be reachable in the path)
- run the compilation script for your system (you may have to adjust the references in
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.
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.