CIS 673: Computer-Aided Verification, Spring 2020


Instructor: Rajeev Alur ( alur@cis)

Class: Mon Wed 3--4.30


Introduction

How can a programmer verify that the software they have designed works correctly as intended? Computer-aided verification is a sub-discipline of computer science aimed at developing tools and techniques to assist programmers meet this goal. These tools have now reached a level of maturity where they are being integrated in system design in companies such as Amazon, Facebook, Google, and Microsoft. This course focuses on logical foundations necessary to formalize the question of software verification and algorithmic tools necessary to automate the challenging task of software verification to the extent possible.

Prerequisites

The course assumes basic knowledge of algorithms, data structures, programming languages, computational complexity, and propositional logic. The course requires mathematical maturity, and is appropriate for students who wish to pursue research in formal methods, programming languages, or cyber-physical systems. If you need more information to decide, contact the instructor.

Logistics

Every week, students are expected to read course handouts and participate actively during class. Each student is also expected to do a class project and give a presentation at the end of the semester. There will be no homeworks or exams.

Topics

The exact set of topics will be determined dynamically based on the students' interests. Below is a tentative organization of the course:
Maintained by Rajeev Alur