CIS 673: Computer-Aided Verification, Fall 2014


Instructor: Rajeev Alur ( alur@cis)

Class: Mon Wed 10.30-Noon, Towne 305


Introduction

How can a designer check that the system (s)he has designed works correctly? Can an airline control system fail in a critical way when a piece of hardware fails? Will a cache coherence protocol continue to work correctly when an extra processor is added? Traditionally, designers attempt to answer such questions using simulation over selected sample cases. As computer systems become more complex and pervasive, simulation-based techniques are not sufficient to assure desired reliability. Model checking and related computer-aided verification techniques are emerging as practical alternatives to simulation for debugging complex systems. These methods allow the designer to verify that a mathematical model of a system satisfies its abstract logical specification. This course is focused on training students in the basic principles of model checking.

Prerequisites

The course requires basic knowledge of algorithms, data structures, programming languages, automata theory, computational complexity, and propositional logic. The course requires mathematical maturity, and is appropriate for graduate students who wish to pursue research in formal methods, software analysis, or related areas. If you need more information to decide, contact the instructor.

Overview

Each week will focus on a selected chapter from Handbook of Model Checking, Springer, 2014. The chapters of this upcoming Handbook are listed below. We can cover only a subset of these, and the selection will be based on the interests of students. The selected chapters will be distributed as reading material in advance.

Logistics

Every week, students are expected to read the chosen chapter, before the lectures, and participate actively during class. Each student is also expected to do a project and give a presentation at the end of the semester. There will be no homeworks or exams.
Maintained by Rajeev Alur