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

CCR-9985239 CAREER：一种形式化编程方法及其在自动验证器开发中的应用。考德威尔本研究的目标是（i）正式程序开发的新方法的发展，其中联合收割机现有的方法来验证和综合;（ii）这些方法的应用到正确的建设验证引擎的发展;和（iii）整合形式化的数学，支持这些方法到本科计算机科学课程。 在程序开发实践中，有时候验证一个已知的程序更方便，而在其他时候，综合是更好的方法。 该研究探讨了在一个单一的框架内结合这些互补的开发模式，以证明复杂的软件工件的正确性的方法。 这项工作主要是在Nuprl系统提供的构造性类型理论的框架内进行的。 这种新的程序开发方法的应用和完善的背景下，努力重新实现自动验证器，模型检查器和决策过程为基础的验证引擎。 数学定义、证明、证明策略和支持这种程序开发模式的定理的数字表示形式上编码了计算机科学的应用数学。 这项研究探索了将这些材料融入大学课堂的新方法。

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.