CIS 673: Computer-Aided Verification, Fall 2016


Instructor: Rajeev Alur ( alur@cis)

Class: Mon Wed 10.30-Noon, Towne 305


Introduction

How can a programmer verify that the software (s)he has 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. 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. The list of topics includes verification conditions, program termination, propositional and first-order logic, SAT and SMT solvers, abstract interpretation and static analysis, software model checking, refinement proofs, modular reasoning, verification of concurrent programs, and program synthesis.

Note: the previous offering of this course, in Fall 2014, focused on model checking and had a significantly different set of topics (link to 2014 webpage).


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 or programming languages. 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.

Schedule


Resources

We will use a collection of survey articles, research papers, and tutorial slides to cover different topics. For a coherent and in-depth introduction to a subset of topics, the following textbook is recommended: For hands-on experience with automated program verification, play with:
Maintained by Rajeev Alur