sett is a simple tool for proving termination of imperative programs using symbolic execution to explore the execution space. From a complete symbolic execution graph, we produce an ITRS (integer rewrite system) whose termination can be checked using mature provers like AProVe.

It takes as input an imperative program with the following features:

  • variables must be declared, e.g., VAR x,y;
  • the initial state, which is given by a line number and the initial values of the program variables,
    e.g., MAIN 1 x=0,y=0;
  • the numbered program statements, which include assignments, conditionals, jumps, and halt (to stop execution). The predefined function input() can be used to read a random value.

An example program follows:

# Example taken from Byron Cook, Andreas Podelski, Andrey Rybalchenko: 
# Proving program termination. Commun. ACM 54(5): 88-98, 2011);

VAR x,y;
MAIN 1 x=0,y=0;

1: x := input();
2: y := input();
3: if (x>0 && y>0) then 4 else 10;
4: if (input()==1) then 5 else 8;
5: x := x-1;
6: y := y+1;
7: jump 9;
8: y := y-1;
9: jump 3;
10: halt;

A technical description can be found in this paper:

  • Germán Vidal. Closed symbolic execution for proving program termination. Submitted for publication. PDF

Check the web interface in the next tab.

Please let me know if you have any question or comment to gvidal@dsic.upv.es.

Source program (you can load in an example and edit it)
Choose a file:        

ITRS generated by complete symbolic execution:

You can copy and paste this program to AProVe or just press the next button...