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

点击翻译按钮获取中文摘要

CCR-9985239CAREER: A Formal Programming Methodology with Applications toDeveloping Automated VerifiersPI: James L. CaldwellThe goals of this research are (i) the development of new methods forformal program development which combine existing approaches toverification and synthesis; (ii) the application of those methods tothe development of correct-by-construction verification engines; and(iii) integrating the formalized mathematics that supports thesemethods into the undergraduate computer science curriculum. Inprogram development practice it is sometimes more expedient to verifya known program, while at other times, synthesis is the betterapproach. The research investigates methods of combining thesecomplementary modes of development within a single framework tojustify the correctness of complex software artifacts. The worklargely takes place within the framework of the constructive typetheory provided by the Nuprl system. This new method of programdevelopment is applied and refined in the context of efforts to securecorrect implementations of automated verifiers; model checkers anddecision procedure based verification engines. The digitalrepresentations of mathematical definitions, proofs, proof strategies,and theorems that support this mode of program development formallyencode the applied mathematics of Computer Science. This researchexplores new ways to incorporate this material in the undergraduateclassroom.