QFIS

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

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

Contents

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)

Installation

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).