Welcome

Welcome to EECS 755 — Software Modeling and Analysis!

This course is an advanced introduction to formal methods, covering specification, verification, and implementation of computer-based systems using the Rocq proof assistant and the Logical Foundations textbook.

A few things to do before the first class:

1. Read the syllabus carefully — pay particular attention to the homework grading policy.
2. Install Rocq by following the installation instructions.
3. Join the class on Canvas if you are not already included.

Looking forward to a great semester.