1. matthewhague
  2. cshore

Overview

HTTPS SSH
C-SHORe:

A verification tool for higher-order recursion schemes and collapsible pushdown
systems using a saturation technique.

More details:

    http://cshore.cs.rhul.ac.uk


INPUT FORMATS:

Examples in examples/input-formats.  We recommend .hrs, .hrsc, and .cpds.

    + .hors -- proprietary input format for higher-order recursion schemes
    + .hrs -- input format used by Kobayashi's TRecS tool (performs type 
              inference)
    + .horsc -- proprietary input format for higher-order recursion schemes with
                case statements
    + .hrsc -- input format for higher-order recursion schemes with case
               statements based on .hrs (performs type inference)
    + .cpds -- proprietary input format for collapsible pushdown systems.


DEVELOPERS:

Christopher Broadbent
Arnaud Carayol
Matthew Hague
Olivier Serre


USABILITY:

See CRAPL-LICENSE.txt


COMPILATION AND RUNNING:

    1) Make sure you have Scala and sbt installed.
    2) run using ./run.sh <file>
       the run command automatically compiles the code.

How to generate a jar file.

    ./run.sh uses sbt to launch the application, this is a bit slow.  You can
    generate a jar instead by running

        sbt assembly

    and then

        java -jar target/HO-assembly-0.1.jar <file>