The fundamental goal of this project is to raise the competence of software developers to create and verify reliable software by improving the ability of undergraduate computer science students in reasoning about the correctness of computer programs. To reach this goal, this project has one technical objective and two educational objectives. The technical research objective is to develop practical verification techniques suitable for teaching in undergraduate computer science courses. The educational research objectives are to develop and disseminate learning modules and materials on program verification and to integrate formal program verification - reasoning based on mathematics - into the undergraduate computer science and engineering curriculum.
The mathematics to achieve this project's educational goals of integrating program verification into the undergraduate curriculum is through the use of sets and functions. An annotation notation incorporating recent advances in specification languages is developed to document programs as functions from input values to output values. The annotation notation supports a spectrum of formality, from informal to fully mathematical, to assist an incremental integration into the curriculum. A functional verification approach, which supports a natural, intuitive, forward reasoning, is extended for modular verification of object-oriented programs, and lightweight tools are developed for teaching and learning functional specification and verification. An incremental integration to the curriculum is achieved by first delivering an experimental course on program verification and then, using this experience as a guide, introducing problem-based learning modules throughout undergraduate courses. The approach is demonstrated by integrating modules into the undergraduate computer science curriculum from the introductory courses to the senior capstone course.
