This is a list of 'Frequently Asked Questions' (including some that I made up):
Check the schedule page.
It's an introduction to the foundations of what is ususally referred to as Formal Methods. The goal of such methods is to improve the reliability of (software of hardware) systems through one form or another of mathematical reasoning. The idea is that such a rigorous approach can provide designers with a better understanding of the systems they built. It can help assert desirable properties of a system in a strong way, or find errors that other approaches (such as testing) might fail to catch.
There is a wide variety of formal methods. Some are more automatic than others. Some are more limited in scope than others. Some focus on verifying properties of systems, while other are more interested in finding mistakes and bugs. Some methods have been designed specifically for hardware systems. Some are tailored to object-oriented programs. Some are focusing on concurrent and reactive systems. All these techniques rely on a common foundational basis. This course is about (some of) these foundations.
Yes. This means that undergraduates can take this course to fulfill their theory requirement. Although this is not a "traditional" CS theory course, it does include its share of logic, proofs and other discrete maths topics.
Yes, for the first part (logic and the other mathematical tools that we need); no, for the second part (program specification and verification). Students are required to have (access to) a copy of the book. Check the textbook page more more information.
Check the explanation on the slides
D-.
No. Everybody is graded on the same set of assignments and exams. It's not "à la carte"...
No. If you feel you need a break from programming, this course is for you.
Unfortunately, no. I would need another complete course to focus on tools and assistants for program verification. I'm still looking for a simple tool that would be suitable for this course. Maybe some day...
Who said this course was difficult? :-)
One major difficulty involves reasoning non operationally. This is unusual, especially for programmers. We need to describe what it is that a program is achieving (it's specification) without explaining how it does it (its algorithm). It seems that CS students are often better at writing algorithms than they are at writing specifications. A second difficulty is to formalize this specification using mathematics, which requires knowledge of symbolic logic. Finally, there are correctness proofs, which can sometimes be tricky.
Programming languages. Check it here.
>
Last modified: Thu May 10 00:29:30 EDT 2007