KIND VERIFIER INSTALLATION

The Kind verifier written in Ocaml and reads files in (a subset of) the
synchronous dataflow language Lustre.

Information and downloads concerning Ocaml can be found at
http://www.ocaml.org

Information on Lustre can be found at the Verimag Synchron site
http://www-verimag.imag.fr/~synchron/

===================

Installation:

Precompiled executibles for Kind can be found in the /bin directory of the 
distribution for a few operating systems.  Or you can compile it yourself:

The Kind verifier is written in Ocaml.  Compiling and running it 
requires a local Ocaml installation.  See http://www.ocaml.org.

It also requires:

  - the OCamlMakefile, by Markus Mottl, available as (4.2.13) from
       http://ocaml.info/home/ocaml_sources.html

  - a compatible SMT solver, including
       * Yices, available at http://yices.csl.sri.com/
         Get the latest version, with GMP statically linked
         (this requires a click-through license agreement)
       * CVC3, available at http://www.cs.nyu.edu/acsys/cvc3/ 
         (version 1.5 or later)

First unzip the Kind tarball and copy the OCamlMakefile into the base Kind 
directory.

To compile Kind, change to the base Kind directory and type "make".  The 
executable kind will be created in the current directory.

To create ocaml html documentation for the source (to be created in 
doc/), type "make htdoc". (The OCamlMakefile also supports various
other end formats for documentation, such as man and latex.)

Copy the desired solver executable into the Kind directory.

./kind --help will give a list of options

===================

Solvers:

It is possible to use either the CVC3 pre-compiled executable or to compile
your own version.  Similarly, with a command flag, it is possible to use
the pre-compiled Yices executable.

The default operation of Kind uses a wrapper version of the Yices solver.
The wrapper is written in C and, when compiled, calls the Yices (statically
linked) library.  (Yices' command line version's interactive mode is limited 
in the size of formulas it can accept).  Depending on the version of Yices 
you use, you may need to upgrade your compiler version.

It is known that Yices 1.0.9 will compile under RedHat EL 4.0.
It is known that Yices 1.0.18 will compile under RedHat EL 5.0.

To compile yicesw, first define the variable "yices_root" in the script 
"build_yicesw" to point to your Yices installation directory.  
(If compilation fails, it may also be necessary to also modify the libraries 
referenced if compiler errors appear.)

Then run 
  ./build_yicesw

This should create an executable "yicesw", which should be placed in the
same directory as the kind executable.

===================

Running the Kind solver:

Basic operation of Kind is (assuming the Yices wrapper was created):

./kind [options] <lustrefile>

where <lustrefile> is the Lustre source file you wish to check.

common options are:
  -help    (command line info)
  -version (version & copyright info)
  -path    (abstraction with "path" refinement strategy)
  -loop    (enable path compression)
  -bmc     (only look for counterexamples via BMC)

If using the command-line version of Yices, use the option
  -yices_exec
with a copy of the Yices executable in the current directory.
Similarly, to use CVC3 as the solver, use the option
  -cvc3
with a copy of the CVC3 executable in the current directory.

The various [options] are more fully described in the README file.


