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 11am - 1 pm
Lecture time: Tuesday and Thursday 9:40-11am
Lecture room: Sproul hall 2360
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 to prove the partial and total correctness of sequential programs. We also study abstract syntax, operational semantics and basic type systems and their proof of soundness.

 Suggested Reading

- The Calculus of Computation: Decision Procedures with Applications to Verification. Aaron R. Bradley and Zohar Manna. 2007.
- Types and Programming Languages. Benjamin Pierce
- Software Foundations. Benjamin Pierce and others.


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.