Documentation

Input format

The input format of the VVT is based on the SMTLib2-format. The format describes the transition relation of the program as an extended logical circuit. The basic structure of a program consists of

A state vector describing the types of the state variables
An input vector which contains nondeterministic variables
Definitions of gates
The definition of the next state
The definition of the initial state
Properties that should be verified

(program
  (state ...)
  (input ...)
  (gates ...)
  (next ...)
  (init ...)
  (property ...)
  )

The state vector is a list of pairs of variable names and types. For example, if your program has an integer named “x” and a boolean called “c”, the state vector would look like this:

 ...
 (state (x Int) (c Bool))
 ...

The input vector has the same format as the state vector. For example, a program with a boolean input variable “y” would have the input vector:

 ...
 (input (y Bool))
 ...

Gates allow you to bind expressions to names to avoid repetition of common expressions. For example, if you wanted to use the expression “x+x” more than once, you could bind it to the name “twox” like so:

 ...
 (gates (twox Int (+ x x)))
 ...

To specify how the successor state is defined, we add a definition for every state variable in the “next” list:

 ...
 (next (x (ite c twox x))
       (c (and c y)))
 ...

The starting state of the program is specified using the “init” list:

 ...
 (init (x 0) (c True))
 ...

Properties that should be verified by either vvt-verify or vvt-bmc can be specified in the list of properties. For example, to specify that “x” is always smaller than 100, we can say:

 ...
 (property (< x 100))
 ...