HIP/SLEEK extension for the Barrier Logic

This prototype is an extension of the HIP/SLEEK verification toolset to include the verification of programs with barriers. The prototype was developed in support of

  • my thesis submission: "Efficiently Verifying Programs with Rich Control Flows"
  • the "Barriers in Concurrent Separation Logic: Now with Tool Support" submission
As a start, please find below : s
  • A brief introduction to hip/sleek ( hip , sleek )
  • The prototype executable and examples: ( hip&sleek )
    The archive contains:
    • The hip and sleek executable compiled under the Ubuntu 10.04.1 LTS
    • Basic examples for hip and sleek, including the examples used for the pruning experiments, the fractional shares entailments an the examples on barriers
  • sc-linux-hip.tgz contains the hip and sleek executables compiled for the scientific linux distribution
  • HIP/SLEEK requirements:
    • the mona prover to be installed
    • the omega calculator (oc) to be placed in a path folder (e.g. /usr/local/bin/). We provide an omega calculator version which is slightly modified, which we recomend (the default version works as well) ( oc )
    • The prelude files ( zip ) to be accessible, preferably in the same directory as the HIP/SLEEK executable
  • Running:
    • with specialization: ./hip --eps [input_file]
    • without specialization: ./hip [input_file]
    • detailed timings can be obtained by adding the "--epi" flag
    • to verify examples with bags the mona prover needs to be employed by adding the "-tp om" flag
    • to obtain a full list of options: ./hip --help