Fall 2020: Formal Verification of Hardware and Software Systems

The course will be based on reading classic papers on software and hardware verification as well as more recent papers that describe advances in automated reasoning algorithms and their applications to verification. A theme of the course will be to find common threads that tie together the seemingly‐disparate methods used in HW and SW verification. Students can expect to learn how to encode software programs and hardware circuits as transition systems, and how to develop suitable abstractions for checking control‐centric properties. Additionally, they will have hands‐on experience with a variety of existing reasoning and verification tools and the option of developing extensions to these tools. The course work will consist of a few short assignments to help the students master the main technical issues and semester‐long individual or group projects selected by the students.