The main deliverables (in chronological order) will be:
1. 1-2 page proposal, with precise problem definition, literature survey, and timeline; (5 % towards final grade)
2. 1-2 page preliminary report, describing progress on the timeline; (5 %)
3. 4-6 page final report: This should read like a conference paper, must use at least 10 pt font; (~20 %)
4. Project presentation and possibly demo. (~20 %)
Here is a list of suggested projects (Berkeley campus access only).
Course Topics and Schedule (subject to change)
Lec. | Date | Topics | Suggested Readings | Homeworks & Milestones |
---|---|---|---|---|
1 | 1/17 |
Introduction
(PDF)
|
||
Part I: Computational Engines | ||||
2 | 1/22 |
Boolean Satisfiability - Part I
(PDF)
|
L. Zhang thesis (Ch. 2) | |
3 | 1/24 |
Boolean Satisfiability - Part II
(
PDF of Main Lecture,
Example 1,
Example 2,
BCP Intro.
BCP Example
)
|
L. Zhang thesis (Ch. 3, 4) | |
4 | 1/29 |
Binary Decision Diagrams
(
PDF
)
|
R. E. Bryant's 1992 Computing Surveys paper, MC Sec. 5.1 | |
Part II: Foundations of Model Checking -- Systems with Boolean State | ||||
5 | 1/31 |
Models and Properties
(
PDF
)
|
MC Ch. 2 | HW 1 out, Project topics announced |
2/5 | Class cancelled (grad admissions meeting); will be rescheduled -- Decide on your project topics! | |||
6 | 2/7 |
Finite-State Model Checking -- Introduction
(
PDF
)
|
MC Ch. 3 | |
7 | 2/12 |
Explicit-State Model Checking
(
PDF
)
|
MC Ch. 9: 9.1, 9.2; SPIN Ch. 6, 8 | |
8 | 2/14 |
More Explicit-State Model Checking
(
PDF
)
|
SPIN Ch. 8, 9; MC Ch. 10 | HW 1 due; HW 2 out |
2/19 | President's Day Holiday | |||
9 | 2/21 |
Symbolic Model Checking with BDDs
(
PDF
)
|
MC Ch. 5, Ch. 6: 6.1, 6.2 | Project proposal due |
10 | 2/23 |
More Symbolic Model Checking and Abstraction
(Make-up lecture, 540 Cory 11 - 12:30) ( PDF )
|
MC. Ch. 6: 6.3, 6.4, 6.6, Ch. 13: 13.1 | |
11 | 2/26 |
Abstraction (contd.) and Symbolic Model Checking without BDDs
(
PDF
)
|
||
12 | 2/28 |
More Abstraction; Notions of Simulation and Language Equivalence
(
PDF
)
|
[McMillan 2003], [McMillan 2005], Ch. 11 |
HW 2 due; HW 3 out |
13 | 3/5 |
Compositional Reasoning and Symmetry; Mu-Calculus
(
PDF
)
|
MC Ch. 14, 12, 7 | |
14 | 3/7 |
Pushdown Model Checking
(
PDF
)
|
S. Schwoon's thesis (Sec. 2.1 - 2.3, Ch. 3) | |
15 | 3/12 |
Games and Verification
(
PDF
)
|
F. Mang's thesis | |
16 | 3/14 |
Model Generation from Traces
(
PDF
)
|
HW 3 due | |
Part III: Research Frontiers | ||||
17 | 3/19 |
Satisfiability Modulo Theories
(
PDF
)
|
[Barrett et al. 1998]; [Bryant et al. 2007] |
|
18 | 3/21 | No regular class. Instead, attend Prof. Ranjit Jhala's lecture on software model checking on 3/22, from 11:30 am - 1 pm, in 405 Soda | ||
3/26 | Spring recess | |||
3/28 | Spring recess | |||
19 | 4/2 | No regular class. Instead, attend paper presentation on Runtime Monitoring in Prof. Sen's CS 294-5 class on 4/3, 11:30 am - 1 pm in 405 Soda | ||
20 | 4/4 |
Learning Algorithms in Model Checking: Abstraction and Assume-Guarantee Reasoning
(Guest lecture by Dr. Anubhav Gupta, Cadence Berkeley Labs) ( PDF ) |
Project preliminary report due by e-mail to Sanjit on 4/6 | |
21 | 4/9 | Coverage Metrics for Formal Verification (Wenchao Li) ( PDF ) |
[Hoskote et al. 1999]; [Chockler et al. 2006] |
|
4/11 | Class rescheduled to Friday (Sanjit at SRC review) | |||
22 | 4/13 |
Error Localization and System Repair
[11 am - 12:30 pm, in 540 Cory]
(Shyam Rajagopalan) ( PDF )
|
[Groce et al. 2005]; [Griesmayer et al. 2006] |
|
23 | 4/16 |
Parallelism in Verification
(Rhishikesh Limaye)
(
PDF
)
|
[Melatti et al. 2006]; [Feldman et al. 2004] |
|
4/18 | Class cancelled (Sanjit away at DATE conference) | |||
24 | 4/23 |
Combining Multiple Tools and Techniques
(Sungmin Cho)
(
PDF
)
|
[Ho et al., 2000] [Gulavani et al., 2006] |
|
25 | 4/25 | Model Checking Hybrid Systems (Jia Zou) ( PDF ) |
[Alur et al., 1995] [Agrawal and Thiagarajan, 2005] |
|
26 | 4/30 |
Computational Logic and Security
(Susmit Jha)
(
PDF
)
|
[Blanchet 2006] [Barth et al., 2006] |
|
27 | 5/2 |
Specifications: Choice of logic, and synthesis
(Narayanan Sundaram)
(
PDF
)
|
[Vardi 2001] |
|
5/7 | Project presentations (9:30 am to 12 noon in 540 Cory) | Final project report due |