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.
