CAREER: A Formal Programming Methodology with Applications to Developing Automated Verifiers

University Of Wyoming, Laramie WY

Investigators

Abstract

CCR-9985239 CAREER: A Formal Programming Methodology with Applications to Developing Automated Verifiers PI: James L. Caldwell The goals of this research are (i) the development of new methods for formal program development which combine existing approaches to verification and synthesis; (ii) the application of those methods to the development of correct-by-construction verification engines; and (iii) integrating the formalized mathematics that supports these methods into the undergraduate computer science curriculum. In program development practice it is sometimes more expedient to verify a known program, while at other times, synthesis is the better approach. The research investigates methods of combining these complementary modes of development within a single framework to justify the correctness of complex software artifacts. The work largely takes place within the framework of the constructive type theory provided by the Nuprl system. This new method of program development is applied and refined in the context of efforts to secure correct implementations of automated verifiers; model checkers and decision procedure based verification engines. The digital representations of mathematical definitions, proofs, proof strategies, and theorems that support this mode of program development formally encode the applied mathematics of Computer Science. This research explores new ways to incorporate this material in the undergraduate classroom.