n

CS 592: Advanced Topics in Verification: Verifying Systems at Scale

Meeting Time

Tuesday, Thursday: 1:30 - 2:45
LWSN 3rd floor lab

Instructor

Suresh Jagannathan
LWSN 3154J
Ph: x4-0971
email: suresh@cs.purdue.edu

Course Overview

The past decade has witnessed tremendous advances in the application of formal methods to real-world problems. These advances have been realized through new proof methodologies, improvements in automated theorem proving (SAT and SMT), and the emergence of mechanized proof assistants as a viable vehicle for proof engineering. In this seminar, we will undertake a number of case studies that examine how these tools and methodologies enable scalable and realistic verification of deployed, widely-used software systems. We will examine exemplar instances across six different domains: compilers, language-based verifiers, concurrency, distributed systems, microkernels and operating systems, and neural networks. Our focus will be to glean insights about the tools and techniques used in these systems that enable modular, compositional, and scalable verification.

By the end of the class, students should be comfortable with the benefits and limitations of modern verification tools, various verification methodologies (e.g., types, abstract interpretation, model-checking, etc.) and proof techniques (e.g., refinement, separation logic, rely/guarantee, etc.), and the range of safety properties found in these different domains that are amenable for verification. Most importantly they should gain fluency in proof engineering - understanding mechanisms to enable scalable, maintainable, and compositional formal reasoning, critical for deploying verification and formal methods in real-world settings.

Prerequistes

It is assumed that students taking this class would have had exposure to a graduate-level programming languages foundation class.

Paper Assignments

A google sheeets with a list of papers, students assigned to lead them, and presentation dates can be found here. Students should fill-in slots based on their interests and can collaboratein the presentations. New topics and papers are welcome. Presentation leads should communicate the papers that will be discussed on Piazza ahead of time, and ideally identify discussion topics for the class to consider prior to the meeting.

It is *strongly* encouraged that students not only just read the papers, but closely examine the tools these papers and built-on and the artifacts they produce. It is expected that presentations will discuss both the technical contributions of the papers being discussed as well as giving subjective analysis of these tools.

Lectures

August 23 - August 27, 2021
  1. Introduction