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:
MAIN 1 x=0,y=0;
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:
Check the web interface in the next tab.
Please let me know if you have any question or comment to
|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...