THE KIND LUSTRE VERIFIER

Kind is an inductive verifier and checker for Lustre programs.

-----

INSTALLATION

You will need a copy of the Ocaml compiler, the OCamlMakefile, and one of the
solvers Kind supports (currently Yices) installed.

See the file INSTALL for more information.

---

If you desire Kind to create variable dependency graphs, you must have the
"dot" program from the graphviz suite installed and located on your default
execution path.  (But if not, then don't worry.)

---

LUSTRE FILES:

Kind currently does not support included files, and there can be no forward
references of nodes.  There is only very limited support for non- linear
arithmetic, records, and the "when" operation.  We do not support arrays,
recursive calls, or user-defined types at this time.

The topmost node to be checked should include the special comment line
  --%MAIN
somewhere in its body.  If no node includes this line, then the last node
in the source file is taken to be the topmost node.

Properties to be checked should appear in special comment lines in the body of 
the topmost node:
  --%PROPERTY <lustre property>
where <lustre property> is a Lustre Boolean expression, ending with a 
semicolon.  Multiple property lines are conjoined.

Example:
node sum (x:int) returns (sum:int);
let
  sum = x -> x + pre sum;
tel

node resetsum (x:int; r:bool) returns (sum:int);
let
  sum = if r then 0
        else (x -> x + pre sum);
  --%MAIN
  --%PROPERTY if r then sum=0 else sum <> 0;
tel
~                                                                               
~           

---

RUNNING KIND:

This assumes kind is running with the latest version of Yices, with the 
user-compiled wrapper file "yicesw" (see INSTALLATION).  To utilize other 
solvers, use the appropriate command line flags, below.

Usage:
  kind <options> lustre-file

Kind options:

Overall program behavior:
  -n              Stop after n iterations (default 200)
  -t              Stop after n seconds (default max_int)
  -bmc            Only performs BMC (default: false)
  -step_size      Only check induction every n steps (default 1)
  -sal_ind        Perform SAL-like induction behavior at step n 
                  (default false)

Solver options:
  -yices_exec       Use Yices executable as solver (default: yices_wrapper)
  -cvc3             Use CVC3 executable as solver (default: yices_wrapper)
  -bv               (for CVC3 only) use bitvectors to represent Boolean terms 
                    (default: false)
  -flags            Pass string to solver command line (default: n/a)
  -single_solver    Uses 1 solver instance for both ground & symbolic formulas 
                    (default: false)
  -separate_solvers Uses 2 solver instance, one each for ground & symbolic 
                    formulas (default: true)
  -define_mod_div   Include definitions for mod & div (may be incomplete) 
                    (default: false) This is necessary for Yices 1.0.9 wrapper
  -buffer_limit     Try decreasing this if the program hangs early 
                    (default 200000)

Definition generation:  
  -aggdef      Use aggregate definitions (default: false)

Output options (all default false):
  -debug       Include debugging output 
  -quiet       Only return final answer (default: true)
  -verbose     Include more details in output
  -noscratch   Do not log scratchwork to disk (default: log to disk)
  -only_inputs Only print inputs in counterexamples 
  -dot         Prints dot graph of dependencies 
  -dotall      Outputs all abstraction dependency graphs to graphXXX.dot 

Optimization/tweaking (may be experimental, all default false):
  -no_inlining         Do not attempt variable inlining
  -aggressive_inlining Perform aggressive inlining up to complexity n 
                       (default: 0)
  -abstract_pres       Abstract terms below a pre
  -abstract_ites       Abstract ITE terms
  -abstract_control    Abstract ITE and boolean terms

Path compression options (all default false):
  -loop                   Include loopfree constraint formulas + term check 
  -compression            Include path compression but not term check 
  -finite_term            Include the finite termination check constraint, but 
                          no loopfree constraint
  -static_loop            Use a statically calculated loopfree constraint 
  -initial_compression    Include compression against initial configurations 
  -no_check_compression   Do not check compression is fully defined 
                          (incomplete)
  -interleave_term_checks Perform term checks every after a step 
  -compression_in_checker Adds constraints to abstraction checker

Abstraction/refinement (all default false):
  -pre_refine_state      Refine state variables initially
  -abs                   Use fine-grained abstraction refinement
  -core                  Use core-based abstraction refinement
  -path                  Use path-based abstraction refinement
  -subtree               Use subtree-based abstraction refinement
  -incr                  Use increasingly coarser-grained refinement
  -no_inductive_check    Do not check refinement in inductive step (adds 
                         incompleteness, but often faster)
  -force_refinement      Periodically force a refinement step with 
                         frequency n (default max_int)

Help:
  -version Print version & copyright information
  -help    Display this list of options
  --help   Display this list of options


In more detail:

Timeouts:
  -n x: halt once reaching depth x.
  -t x: halt after x seconds.
  -step_size x: (x>0)  If x>1 then only perform induction check every x steps.
  -bmc: run in BMC mode only.
  -sal_ind x: run BMC to depth x, then perform an induction step, then stop.

Solver options:
  -yices_exec: use Yices executable instead of wrapper version.  It should
     be called "yices" and be in the same directory as Kind
  -cvc3: use CVC3 executable as the solver.  It should be called "cvc3" and 
     be in the same directory as Kind
  -bv: (for CVC3 only) use bitvectors to represent Boolean terms
  -flags x: pass the string x (in quotes) to the yices binary
     The wrapper version "yicesw" currently only recognizes the flag "-debug"
  -buffer_limit x: Try decreasing this if program seems to hang early.
     It determines the maximum length of strings sent to the solver; 
     sometimes a too-long string can cause a system hang (a limit on pipe 
     buffers).
  -define_moddiv: certain version of yices did not include definitions 
     of the mod and div functions with the API interface (1.0.9).  While these 
     function are not built in to CVC3, (possibly incomplete) definitions will 
     be automatically included for the CVC3 solver if appropriate without the 
     need for this flag.
  -single-solver: only use one solver instance for both base and step case
  -separate_solver: the default behavior

Induction/BMC behavior (default: k-induction, step size 1)
  -step_size x: (x>0)  If x>1 then only perform induction check every x steps
  -bmc: run in BMC mode only
  -sal_ind x: run BMC to depth x, then perform an induction step, then stop

Output
  -quiet: minimal output(default behavior)
  -verbose: more extensive output
  -debug: include extra (excessive) debugging information in output
  -noscratch: normally Kind produces scratch files detailing all calls to 
     yices for inspection or hand-modification (1 for each solver).  This 
     option does not populate said extra files.
  -only_inputs: Counterexamples generally include all (refined) variables.
     Ths limits them to only display input variable values.

  These require the dot graphing program to be installed and produce .dot and 
    .gif files:
  -dot: generate a dot graph of static variable dependencies
  -dotall: generate dot graphs of variable dependencies as they are refined

Abstraction options (default: no abstraction)
  -pre_refine_state: refine the variables to be used in path compression ahead 
    of time
  -abs: use basic abstraction, 1 variable refined per iteration
  -core: refine multiple variables per iteration, based on analysis
  -path: use "path refinement", several related variables refined per iteration
  -subtree: refine all variables that an identified abstract variable depends
     on in one iteration (most aggressive refinement)
  -incr: refine gradually more and more variables per iteration
  -no_inductive_check: Do not check for refinement in inductive step (adds 
     incompleteness, but often faster).
  -force_refinement: Periodically force a refinement step (even if not
     otherwise called for).  This can address problems in a refinement 
     strategy that might otherwise not be converging quickly enough.

Path compression options (default: no path compression)
  -loop: full path compression + termination check
  -compression: Only perform path compression (in inductive check)
  -finite_term: termination check only
  -static_loop: statically determine the maximum path compression formula
     (This would be redundant with -pre_refine_state and vice versa)
  -interleave_term_checks: Only perform termination checks prior to an 
     induction step check (step_size-1) (useful in combination with larger
     step sizes)

General behavior & tweaks (default: false)
  -aggdef: Use aggregate definitions (alternate translation). This is not 
     available in combination with abstraction (and is more likely to result 
     in buffer overflow errors).
  -no_inlining: Do not attempt any variable inlining (usually redundant 
     variables are unified)
  -aggressive_inlining: Perform a more aggressive version of inlining, up to
     an estimated maximal complexity of the resulting definitions
  -abstract_pres: Abstract (flatten) terms below a pre as a preprocessing step
  -abstract_ites: Abstract (flatten) ITE terms as a preprocessing step
  -abstract_control: Abstract (flatten) ITE and boolean terms as a 
     preprocessing step

---

Output:

Upon successful completion, Kind will output whether the property holds or 
provide a counterexample to the user, as well as information as to the
depth of the search.

Some examples include:

; 5 step is Valid.
; +++ The property holds. +++
; Done.

and

; 7 base is Invalid.
; Counterexample trace:
;                       Instant
; variable                0   1   2   3   4   5   6
; OK                      1   1   1   1   1   1   0
; a                       0   1   0   1   0   1   0
; b                       0   0   1   1   0   0   0
; c                       0   0   0   0   1   1   0
; Done.

(Here the counterexample lasts seven time ticks.)  Variables mentioned in 
counterexample should correspond to the names of variables in the
topmost node -- variables in sub-nodes will typically consist of their node's
name, an instance number (unique for each call), and the variable name.  For 
example, the variable IntCounter_233_x would refer to the variable "x" in
the instance 233 of node IntCounter (the instance number is based on the
character position of the call in the source program, so this call to 
IntCounter would have been at approximately the 233rd character of the
original program).

When in -quiet mode, counterexamples will not be output.

In -verbose mode, additional information about the search process will be
output, including the step-by-step results of the verification process, 
how the abstraction is being refined, and if spurious counterexamples are
detected.

By default, Kind keep track of all calls made to the solvers in up to 3 files:
<xx>.yc, <xx>.yc_2, and <xx>.yc.ck for the Yices solver (placed in the same 
directory as the Lustre source).  <xx>.yc contains the commands sent to the 
ground (inductive base case) solver, <xx>.yc_2 contains the commands sent to 
the symbolic (inductive step case) solver, and <xx>.yc.ck contains commands 
sent to the counterexample checking solver.  These files should be able to be 
examined and fed directly into Yices in the event of unexpected behavior.

In all cases, <xx> is the original lustre program filename.

(For the CVC3 solver, the filenames substitute "cvc" for "yc".)

The command line flag -noscratch will not populate these files.

---

Contact:

For more information (or if you are finding Kind useful), please contact
either George Hagen (george-hagen@uiowa.edu) or Cesare Tinelli 
(tinelli@cs.uiowa.edu).
