ddlTerm

ddlTerm is a data-driven loop termination analysis tool

Install

Download the built docker image directly. Then:

docker load -i ddltermartifact.tar

Run Experiments

Start the docker image (replace `/path/to/a/directory/to/save/the/result`)

docker run -it -v /path/to/a/directory/to/save/the/result:/log --tmpfs /tmpfs --cpus=1 ddltermartifact:latest

Run the experiments (e.g. the main experiment in our paper)

cd ddlTerm
python3 experiment/scripts/RunTasks.py experiment/scripts/configurations/ExpMain/LeNLeMixed_Standard.xml

For a precise result, we suggest:

using tmpfs to reduce the time of IO. (By default, tmpfs has been used in docker running)

setting the CPU limit to one core using cgroup. (By default, CPU limit has been used in docker running)

updating the timeout setting in configuration XML files according to the performance of your machine.

The baseline in Our Paper:

If you want to make a comparative experiment, please follow the install instruments for our baseline tools.

AProVE

Ultimate Automizer

MuVal

FreqTerm

Remember to set the cpu limit to one core using cgroup or by the parameter --cpus if using docker.

The benchmarks locate in experiment/benchmarks.

C-style can be used for AProVE, Ultimate Automizer and MuVal.

Horn-style can be used for FreqTerm.

We provide some useful scripts in experiment/baseline.scripts to run the experiments for AProVE, Ultimate Automizer and FreqTerm. You can modify the path in the scripts to run these tools. We hope these scripts are useful for you.