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 where 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 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: .yc, .yc_2, and .yc.ck for the Yices solver (placed in the same directory as the Lustre source). .yc contains the commands sent to the ground (inductive base case) solver, .yc_2 contains the commands sent to the symbolic (inductive step case) solver, and .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, 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).