QFIS: quantifier-free integer sequences

What is QFIS

QFIS is a static program verifier for imperative programs working on sequences of integers and annotated with formulae in the quantifier-free fragment of the theory of integer sequences. QFIS generates verification conditions from an annotated program by backward reasoning. The verification conditions are translated into SMT input files and CVC3 tries to discharge them. QFIS reports the results of verification back to users.

QFIS can be used as an intermediate language for verification, and as a domain-specific program verifier.

Download QFIS

QFIS is implemented in Eiffel and available both in source and compiled versions under the GPL license.

• Version 0.1 (released 24 March 2011, compiled with EiffelStudio 6.7)
• Version 0.2 (released 19 May 2011, compiled with EiffelStudio 6.7)
• Version 1.0 (released 3 May 2012, compiled with EiffelStudio 7.0)
  • Source and pre-compiled GNU/Linux 64-bit version: download.
  • Pre-compiled GNU/Linux 32-bit version: download.
    (Install the 64-bit package and then replace the content of subdirectory bin with this 32-bit build).
  • User manual (includes installation instructions and a tutorial example).
  • General information about the theory of integer sequences implemented in QFIS.

Video demo of QFIS

In this video demo, you can watch the tutorial example also available in QFIS's manual. Make sure to watch it in HD full-screen for best readability.