GA Tech Research Corp - GA Institute of Technology Manolios

"CRCD/EI: Integrating Functional Computer-Aided Reasoning into the Computer Science Curriculum"

This project involves the development of tools, courses, modules, and self-paced online materials that integrate computer-aided reasoning into the Computer Science (CS) curriculum. This project is novel in undergraduate CS education. The use of a state-of-the-art theorem proving technology (ACL2) permits students to get instant, reliable feedback, thereby enabling effective learning and self-paced study. ACL2 is a tool consisting of a functional programming language, a logic, and a theorem-prover, that has been used to prove some of the largest and most complicated theorems ever proved about commercially designed systems. The project involves at least two research challenges: taking a necessarily complex, state-of-the-art, theorem proving system and teaching undergraduates how to be effective users in a portion of a semester, and developing effective courses in other areas, such as hardware design and object oriented programming, that are based on the use of computer-aided reasoning. A sequence of mathematical concepts and mechanical tools, with well-designed graphical user-interfaces, allow students to gradually and seamlessly master ACL2. Integration of computer-aided reasoning into current curricula is accomplished through two courses that make essential use of these tools, thereby giving students a deeper and more complete understanding of the material. The courses cover the following topics: computer organization and design, object-oriented programming using the JVM, theorem proving, and formal methods. One of the undergraduate courses focuses on computer organization and design and the other on the Java Virtual Machine (JVM). In these two courses, computer-aided reasoning is used to give students a deeper understanding of the material. They are required to think about the properties systems and components under consideration should enjoy and how to prove that these properties do in fact hold.

Agency
National Science Foundation (NSF)
Institute
Division of Information and Intelligent Systems (IIS)
Application #
0844078
Program Officer
Ephraim P. Glinert
Project Start
Project End
Budget Start
2008-03-13
Budget End
2009-08-31
Support Year
Fiscal Year
2008
Total Cost
$210,303
Indirect Cost
Name
Northeastern University
Department
Type
DUNS #
City
Boston
State
MA
Country
United States
Zip Code
02115