Home / Teaching / CS 246

 CS 246: Advanced Verification Techniques

 General Information     

Instructor: Mohsen Lesani
Instructor's email: lesani@cs.ucr.edu
Instructor office hours:  Tuesday and Thursday 10 - 12 am
Lecture time: Tuesday and Thursday 8:10 - 9:30 am
Lecture room: WCH 143
Prerequisites: CS 111, CS 141, CS 150, or equivalents or consent of instructor.
Offering: 4 units. 3 hours lecture, 3 hours outside research. It may be taken Satisfactory (S) or No Credit (NC) with consent of instructor and graduate advisor.

 Course Description

Recent studies show that the global cost of software and hardware bugs is hundreds of billion dollars annually. Aircraft, space shuttles, self-driving cars, medical devices and Internet services are a few use cases that require reliable systems. In the last decade, the verification community has brought tools to assist engineers in building reliable computing systems. We are at the beginning of the new era of verified (rather than tested) computing products.

The goal of this course is to introduce the students to the theory and practice of program specification and verification.

In this course, we will study propositional logic, first-order logic, and commonly used first-order theories and their satisfiability decision procedures. We will work with the state-of-the-art constraint solving tools. We will also study programming using dependent types and interactive theorem proving using higher order logics. We will work with the state-of-the-art functional programming languages and theorem provers. We will study Hoare logic and separation logic to prove the partial and total correctness of sequential programs. We will also look at correctness conditions for concurrent programs including sequential consistency, linearizability and serializability. We will study rely-guarantee and concurrent separation logic to reason about concurrent programs.

 Suggested Reading

- The Calculus of Computation: Decision Procedures with Applications to Verification. Aaron R. Bradley and Zohar Manna. 2007.
- Software Foundations. Benjamin Pierce and others.
- The Art of Multiprocessor Programming. Maurice Herlihy and Nir Shavit. 2008.
- Papers that will be announced.


Regular class attendance is required.

The students will form groups of two, focus on a specific topic, survey and compare previous research projects on that topic and offer a presentation or submit a report. Note that it is not expected that students prepare a paper publishable in a conference in a quarter. The goal is that the students learn about the current topics in verification and develop their review, analytical and idea development skills.

Grading: 50% midterm exam, 50% Final report
The students are allowed to consult books, papers, and the web. However, they must reference all the sources. The students should write the report in their own words.