QuIt is a program verification tool that parses programs and produces first-order logic problems in TPTP syntax. It can be used to check termination of a loop, verify that a loop satisfies a given specification, or generate loop invariants.
The programs must be given in a dedicated guarded command language. Some key features of the language are:
- at every iteration, the first command whose guard evaluates to true is exectuted
- if a command is executed, all its assignments are performed in parallel
- if no guard is true, or if the optional loop condition is false, the loop is exited
- programs are made of a single loop, but you can specify pre-conditions to describe all possibles program states at the beginning of the execution
- you can specify post-conditions, which are used only in 'verification' mode
See the example programs on the repository for more details.
There are three modes:
- the verification mode generates a first-order problem in which the post-condition is essentially the conjecture, and the hypotheses describe the semantics of the loop. Use a first-order theorem prover to solve the generated problem: if successful, the loop satisfies its specification.
- the termination mode is similar, but the conjecture corresponds to the termination of the loop
- the invariant generation mode generates a set of formulas that describe the semantics of the loop. You can then use a symbol-eliminating first-order theorem prover to generate consequences of these formulas, which are guaranteed to be invariants of the loop.
Any prover that supports TFF (typed first-order) in the TPTP syntax, or the SMTLIB 2 syntax, can be used to solve problems generated by the 'verification' and 'termination' modes. Depending on the options and the input program, the TPTP problem may also contain some theories (i.e. arrays, datatypes) or FOOL formulas, where Boolean terms and predicates are treated similarly. All of these features are supported by Vampire.
Problems generated in 'invariant generation' mode rely on a symbol elimination mechanism. As of today, Vampire is the only prover able to perform symbol elimination. To use symbol elimination in Vampire, run
$ vampire --show_symbol_elimination on -avatar off -nm 0 -updr off <file>
The clauses output by Vampire are loop invariants.
To build the executable you will need to have Cmake installed. For example, you can run the following commands to build the executable
$ mkdir build; cd build
$ cmake ..
$ make