Compositional Termination Analysis
This page presents an experimental implementation of Compositional Termination Analysis, introduced at CAV 2010.
For questions about this implementation and our experiments, please contact Christoph M. Wintersteiger.
There are 1665 benchmark files in the set (one loop per file) and the timeout is set to 1 hr. The table of results and scatter plots are available here: Experimental Results
- Current version (Linux x32): tan-0.2.tgz
- The latest device driver models are available at our benchmarks page.
- An experimental binary (Linux x64): tan-x64.tgz (used in our experiments)
- A 32-bit binary (Linux): tan-x32.tgz
- Our benchmark set (goto-binaries): binaries.tgz
- Download goto-cc. This is to required to compile source files into model files which can then be analyzed by tan. E.g., run
goto-cc -o model source.cto compile
- Run tan on the model, e.g.,
tan --engine cta --unranked-method precondition modelto use the CTA engine with precondition checks. Further options are describe in
Optional External Software
- QuBE (We used an experimental version, which is not available online. Please contact the authors if you're interested in this.)
- Cadence SMV
- Cook, Kroening, Rümmer, Wintersteiger:
Ranking Function Synthesis for Bit-Vector Relations, TACAS 2010.
- Kroening, Sharygina, Tsitovich, Wintersteiger:
Termination Analysis with Compositional Transition Invariants, CAV 2010.
This research is currently supported by a grant from the Swiss National Science Foundation.