Experimental Artifacts for Skipping Refinement

This webpage describes the experimental artificats for skipping refinement work described in CAV 2015 submission.

Download aritifacts archive: ([.tar.gz])

Model-checkers used in the experiments

  1. blimc (ats1 version)
    run command: ./blimc <bound> <aig-name>
    where bound = number of instructions + 2 (in case of stack machine) and
    = number of requests + 2 (in case of memory controller)

  2. IIMC (version 1.3)
    run command: ./iimc-hwmcc13 <aig-name>

  3. Temporal Induction Prover (TIP)
    run command: tip <aig-name>

  4. Super Prove
    run command: super_prove <aig-name>

ACL2 Sedan (ACL2s)

CAV 2015 paper: (http://ccs.neu.edu/home/jmitesh/sks/paper.pdf)

  1. Stack Machine (http://ccs.neu.edu/home/jmitesh/sks/stack-machine)

    This directory contains AIGs used for the comparing running time of model-checkers of IO equivalence and SKS for a JVM-inspired stack machines (STK and BSTK). The operational semantics of the machines are described in the paper.

    It also contains an executable to generate models for stack machines and correctness condition based on IO equivalence and SKS. More details on the usage are provided in the README file in the directory.

  2. Memory Controller (http://ccs.neu.edu/home/jmitesh/sks/memory-controller)

    This directory contains AIGs used for the comparing running time of model-checkers of IO equivalence and SKS for optimized memory controller. The operational semantics of the machines are described in the paper.

    It also contains an executable to generate models for memory controller and correctness condition based on IO equivalence and SKS. More details on the usage are provided in the README file in the directory.

  3. Superword level parallelism compiler transformation (http://ccs.neu.edu/home/jmitesh/sks/scalar-vector)

    A directory containing ACL2s model of the scalar and vector machine for superword level parallelism transformation.

    It also contains the proof script for correctness of the transformation based on SKS. Details of installing ACL2s and certifying are in the README file in the directory.

  4. bat-executables ( http://www.ccs.neu.edu/home/jmitesh/sks/bat-executables )

    A directory containing executables required to generate BAT models and corresponding AIGs using model generators provided in stack-machine and memory-controller directories. Instructions on how to use these executables are given in individual directories.