| |
|
|
|
|
|
|
|
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. |
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
- 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.
|
|
|
|
|
|
|
|
|
|