The presence of subroutines in the form of procedures or functions is as important as it is challenging from the point of view of verification. The challenges include, for instance, the treatment of recursive calls (another possible source of non-termination of program execution) and parameters. The presence of functions, on the other hand, complicates the treatment of expression evaluation, which may now be non-terminating. Also, since expressions may contain multiple function calls, side effects have to be carefully considered.