README.SAS14

OVERVIEW:
This file contains instructions about the tool described in
the SAS'14 paper

  J. Brotherston and N. Gorogiannis.
  Cyclic Abduction of Inductively Defined 
  Safety and Termination Preconditions

If you downloaded the Virtual Machine from the SAS website
you will find the executable "while_abduce.native" which
implements the algorithm described in the paper.  If you 
do not have such a binary, look at the file README.compiling.

Running the executable without options will produce some help 
text explaining its usage.

The command 

make whl_abd-tests

will run the tests discussed in the paper.

NB the Mutant tests were made available to us with permission
and are not included in this image.

To obtain more information from the tests, the shell variable
TST_OPTS will add command-line arguments to while_abduce.native.
For example, the command

TST_OPTS=-s make whl_abd-tests

will produce statistics for each test, including runtimes.
Similarly, the command

TST_OPTS=-sd make whl_abd-tests

will display the simplified inductive definitions abduced for
each test.  Other command-line arguments include producing
LaTeX code for proofs or definitions, displaying proofs and
altering the search parameters.


================================================================================
THEORY:
See doc/papers/SAS14.{pdf,bib}

================================================================================
CONTACT:
Questions and help to get things working: 
  nikos.gorogiannis+cyclist@gmail.com

Github: 
  https://github.com/ngorogiannis/cyclist

URL (papers and software): 
  http://www.cs.mdx.ac.uk/staffpages/nikosgkorogiannis/