ddlTerm

ddlTerm is a data-driven loop termination analysis tool <strong>Install</strong> Download the built docker image directly. Then: <pre><code>docker load -i ddltermartifact.tar</code></pre> <strong>Run Experiments</strong> Start the docker image (replace `<em>/path/to/a/directory/to/save/the/result</em>`) <pre><code>docker run -it -v /path/to/a/directory/to/save/the/result:/log --tmpfs /tmpfs --cpus=1 ddltermartifact:latest</code></pre> Run the experiments (e.g. the main experiment in our paper) <pre><code>cd ddlTerm python3 experiment/scripts/RunTasks.py experiment/scripts/configurations/ExpMain/LeNLeMixed_Standard.xml</code></pre> <strong>For a precise result, we suggest:</strong> 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. <strong>The baseline in Our Paper:</strong> If you want to make a comparative experiment, please follow the install instruments for our baseline tools. AProVE Ultimate Automizer MuVal FreqTerm <strong>Remember</strong> to set the cpu limit to one core using cgroup or by the parameter <code>--cpus</code> if using <code>docker</code>. The benchmarks locate in <code>experiment/benchmarks</code>. C-style can be used for <code>AProVE</code>, <code>Ultimate Automizer</code> and <code>MuVal</code>. Horn-style can be used for <code>FreqTerm</code>. We provide some useful scripts in <code>experiment/baseline.scripts</code> to run the experiments for <code>AProVE</code>, <code>Ultimate Automizer</code> and <code>FreqTerm</code>. You can modify the path in the scripts to run these tools. We hope these scripts are useful for you.