Denison Scientific Association: How to Evaluate Programs that Don't Terminate

If you want to figure out how much memory a program requires, then you need to know what that program does when it runs. Unfortunately, the nicest tool for describing how a program runs—big-step semantics—only works for terminating programs. As a consequence, it is cumbersome to verify the memory requirements of programs that might in principle run indefinitely, like your favorite video game or an airplane’s flight software. However, this need not remain the case: This talk will exhibit the cost analysis tool Automatic Amortized Resource Analysis (AARA), show how its resource-bound guarantees rely on big-step semantics, and then show how big-step semantics can be elegantly altered into big-stop semantics to handle nontermination. Using big-stop semantics, the guarantees of AARA and similar tools can be easily adapted to cover programs that don’t terminate.