CIS 673: Computer-Aided Verification, Fall 2021


Instructor: Rajeev Alur ( alur@cis)

Class: Tues Thurs 12--1.30; Towne 307

Office hour: Wednesdays 4-5pm, Levine 609

Teaching assistant: Konstantinos Kallas ( kallas@seas)


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 PhD students who wish to pursue research in formal methods, programming languages, or cyber-physical systems, and undergraduate/Masters students who want to understand the techniques used in formal verification tools. If you need more information to decide, contact the instructor.

Coursework

Every week, students are expected to read course handouts and participate actively during class. There will be two homeworks, one on program verification using Dafny and one on model checking using SPIN. Furthermore, each student will be required to do a class project. The project can be (1) a case study of applying formal verification to design/debug/understand a system component, (2) an implementation, and its evaluation, to enhance features/scalability of a verification tool, or (3) a project of your choice relevant to the themes of the course. At the end of the semester, each student is required to submit a written report and give a presentation about the project.

Topics (subject to change based on students' interests)


Tools


Resources


Maintained by Rajeev Alur