Ranking Function Synthesis
for Bit-Vector Relations

Termination with SATABS

SATABS This page presents an experimental version of SATABS with a binary reachability engine to prove termination of bit-vector programs. It supports various methods of rank function synthesis.

For questions about the binary reachability engine in SATABS and our experiments, contact Christoph M. Wintersteiger.

Experimental Results

Windows Drivers

Small Benchmarks

To see the results for each of our ranking function synthesis methods, click the links in the following table:


Required Software



This research is currently supported by a grant from the Swiss National Science Foundation.