Program verification as a teaching tool for computer science and software engineering

François Dupressoir

The project will explore the design, implementation and use of program verification and interactive theorem proving techniques and tools for teaching both practical aspects of software engineering, and the theoretical underpinnings of the discipline. This will involve some aspects of programming language theory—to design simplified proof tools sufficient to support teaching without overwhelming, and some aspects of user interactions, as well as some pedagogy research.