Abstract
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.