Logic in computer science: tool-based modeling and reasoning about systems

Recent years have brought about the development of powerful tools for verifying specifications of hardware and software systems. By now, major companies, such as Intel, IBM, AT&T, Siemens, and BT have realized the impact and importance of such tools in their own design and implementation processes as a means of coping with the ever-increasing complexity of chip and software designs. This necessitates the availability of a basic formal training that allows undergraduate students to gain sufficient proficiency in using and reasoning with such tool-animated frameworks. We present an existing course, “Logical Foundations of Programming”, that aims at meeting these educational goals. After describing inherent challenges that such a course faces, we then evaluate this course in the larger context of what logical frameworks, if any, should be taught and where they may be placed in a computer science related undergraduate curriculum