Collaborative Proposal: Integrating Theorem Proving into the Software Engineering Curriculum

协作提案：将定理证明融入软件工程课程

• 批准号: 0632872
• 负责人: Matthias Felleisen
• 金额: $ 7.55万
• 依托单位: Northeastern University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2007
• 资助国家: 美国
• 起止时间: 2007-04-15 至 2010-03-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0632872&HistoricalAwards=false
• 关键词: Collaborative; Proposal; Integrating; Theorem; Proving

Computer Science (31)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.

计算机科学（31）“协作提案：整合定理融入软件工程课程”项目正在创建教育材料，以教授正式方法，以确保软件工程期间的正确性属性。知识分子优点：该项目使用ACL2和Drscheme开发软件工程课程，该课程强调设计和机械化的软件设计和软件质量组件中正确性的证明。 更广泛的影响：该项目正在通过开发一组有20多个完整的项目，用于使用ACL2的软件工程课程，从而影响软件工程教育。 他们通过区域和民族会议的演讲来传播结果。