Termination Analysis by Program Inversion

Automatic methods for discovering program runtime and proving program termination have always been a challenging problem in computer science. We present here a novel and systematic approach for calculating an upper bound of the maximum runtime of functions for a non-trivial class of programs. The proof is based on an induction over a treeof execution traces - a new mathematical data structure. As a consequence, this can also show termination for these functions. The approach uses symbolic-numeric algorithms over a novel mathematical data structure, and can systematically find the maximum runtime for a wide class of functions.