CAREER: Realistic Program Termination Verification: Theory and Practice

University Of Cincinnati Main Campus, Cincinnati OH

Investigators

Abstract

This CAREER project combines a research component--designing a practical approach to program termination verification that includes both theoretical study and actual implementation--with an educational component--undertaking the enhancement, for both undergraduates and graduates, of programming language education. The research on termination verification recognizes that, in practice, the programmer often knows for some reasons that a particular program should terminate if implemented correctly and would therefore find great value in a termination checker able to detect program errors that cause non-terminating program execution. Unfortunately, termination checking in a programming language that supports general recursion is often prohibitively expensive. In order to design a termination checker for practical use, the project explores some recent results on the use of dependent types in practical programming, allowing the programmer to encode into dependent types the metrics needed for ensuring program termination and then use type-checking to verify that the provided metrics indeed suffice. The research focuses on providing a mechanism that truly can be applied in practice.