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.

Agency
National Science Foundation (NSF)
Institute
Division of Undergraduate Education (DUE)
Type
Standard Grant (Standard)
Application #
0633664
Program Officer
Scott Grissom
Project Start
Project End
Budget Start
2007-04-15
Budget End
2010-09-30
Support Year
Fiscal Year
2006
Total Cost
$84,718
Indirect Cost
Name
University of Oklahoma
Department
Type
DUNS #
City
Norman
State
OK
Country
United States
Zip Code
73019