Frequently Asked Questions

This is a list of 'Frequently Asked Questions' (including some that I made up):

• Where and when do classes take place?

  Check the schedule page.

• What is this course about?

  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.

• Is it a theory course?

  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.

• Is there a textbook?

  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.

• How do I join the electronic mailing list?

  Check the explanation on the slides

• What minimum grade do I need to satisfy the CS major requirements?

  D^-.

• I just got my final grade. I'm not happy with it. Is there some extra work I can do to improve it?

  No. Everybody is graded on the same set of assignments and exams. It's not "à la carte"...

• Will we be writing programs?

  No. If you feel you need a break from programming, this course is for you.

• Will we be using software tools?

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

• What makes this course difficult?

  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.

• I loved this course! What else do you teach?

  Programming languages. Check it here.

Michel Charpentier <>