Advanced Topics in Reactive Verification

Thursday, 5:00-6:50 PM
Room 513 WWH
Amir Pnueli

Reaching Me

Amir Pnueli

Course Description

This course studies in greater depth various topics in the field of program verification. It assumes prior knowledge of temporal logic, model checking and deductive verification. Among the topics to be considered, we will consider: As part of the course work, students will be required to import, install, and demonstrate one of the available verification tools for model checking or deductive verification of reactive, real-time, or hybrid systems.

Prerequisites: Some background in algorithm design, familiarity with the language of first-order logic, and knowledge of compiler construction techniques.

Course requirements: Assignments and a term project. Importing, installing, and presenting, one of the publicly available system analysis tools.

Class Presentations

Term Project