The "Collaborative Proposal: Integrating Theorem Proving into the Software Engineering Curriculum" project is creating educational materials to teach formal methods for ensuring correctness properties during software engineering.
Intellectual Merit: This project is using ACL2 and DrScheme to develop a software engineering curriculum that stresses design and mechanized proofs of correctness in its software design and software quality components.
Broader Impact: This project is impacting software engineering education by developing a set of more than 20 fully documented projects for use in software engineering courses that employ ACL2. They are disseminating their results through presentations at both regional and national conferences.
