Korat - Manual

Instructions for Using Korat

Installing Korat

  1. download binary distribution, korat_binaries_bundle.zip
    (requires Java 1.5)
  2. unzip korat_binaries_bundle.zip
  3. download graphviz, and start graphviz.exe to install it (this is needed only for Korat visualization feature)
  4. cd korat
  5. try out some of our examples to make sure that everything is working:
    • java -cp korat.jar korat.Korat --visualize --class korat.examples.binarytree.BinaryTree --args 3,3,3 (runs binary tree example)
    • java -cp korat.jar korat.Korat --visualize --class korat.examples.searchtree.SearchTree --args 3,3,3,0,2 (runs binary search tree example)
    • java -cp korat.jar korat.Korat --visualize --class korat.examples.singlylinkedlist.SinglyLinkedList --args 2,3,3,3 (runs singly linked-list example)
    • java -cp korat.jar korat.Korat --visualize --class korat.examples.doublylinkedlist.DoublyLinkedList --args 2,3,3,3 (runs doubly-linked list example)
  6. enjoy playing with Korat :)

Documentation

Command Line Options

--args <arg-list> (required) comma separated list of finitization parameters, ordered as in corresponding finitization method.
--class <fullClassName> (required) name of the class that contains finitization
--config <fileName> name of the config file to be used
--cvDelta use delta file format when storing candidate vectors to disk
--cvEnd <num> set the end candidate vector to <num>-th vector from cvFile
--cvExpected <num> expected number of total explored vectors
--cvFile <filename> name of the candidate-vectors file
--cvFullFormatRatio <num> the ratio of full format vectors (if delta file format is used)
--cvStart <num> set the start candidate vector to <num>-th vector from cvFile
--cvWrite write all explored candidate vectors to file
--cvWriteNum <num> write only <num> equi-distant vectors to disk
--excludePackages <packages> comma separated list of packages to be excluded from instrumentation
--finitization <finMethodName> set the name of finitization method. If omitted, default name fin<ClassName> is used.
--help print help message.
--listeners <listenerClasses> comma separated list of full class names that implement ITestCaseListener interface.
--maxStructs <num> stop execution after finding <num> invariant-passing structures
--predicate <predMethodName> set the name of predicate method. If omitted, default name "repOK" will be used
--print print the generated structure to the console
--printCandVects print candidate vector and accessed field list during the search.
--progress <threshold> print status of the search after exploration of <threshold> candidates
--serialize <filename> seralize the invariant-passing test cases to the specified file. If filename contains absolute path, use quotes.
--visualize visualize the generated data structures