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

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