See here for a what grading a homework involves and the grading schedule.
The main deliverables (in chronological order) will be:
1. 12 page proposal, with precise problem definition, literature survey, and timeline; (5 % towards final grade)
2. 12 page preliminary report, describing progress on the timeline; (5 %)
3. 46 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).
Here is the project schedule.
Lec.  Date  Topics  Suggested Readings  Homeworks & Milestones 

1  1/18 
Introduction
(PDF)


Part I: Foundations  Systems with Boolean State  
2  1/23 
Boolean Satisfiability  Part I
(PDF)

L. Zhang thesis (Ch. 2)  
3  1/25 
Boolean Satisfiability  Part II
(
PDF of Main Lecture,
Example 1,
Example 2,
BCP Intro.
)

L. Zhang thesis (Ch. 3, 4)  
1/30  Class cancelled  makeup class on 2/17 from 12:30  2pm in Cory 299  HW 1 out, Project topics announced  
4  2/1 
Binary Decision Diagrams
(
PDF of Main Lecture,
BCP Example
)

R. E. Bryant's 1992 Computing Surveys paper, MC Sec. 5.1  
5  2/6 
Models and Properties
(
PDF
)

MC Ch. 2  HW 1 due 
6  2/8 
FiniteState Model Checking  Introduction
(
PDF
)

MC Ch. 3  HW 2 out 
7  2/13 
ExplicitState Model Checking
(
PDF
)

MC Ch. 9: 9.1, 9.2; SPIN Ch. 6, 8  
8  2/15 
More ExplicitState Model Checking
(
PDF
)

SPIN Ch. 8, 9; MC Ch. 10  
9  2/17 
Symbolic Model Checking with BDDs
(
PDF
)

MC Ch. 5, Ch. 6: 6.1, 6.2  HW 2 due 
2/20  President's Day Holiday  
10  2/22 
More Symbolic Model Checking and Abstraction
(
PDF
)

MC. Ch. 6: 6.3, 6.4, 6.6, Ch. 13: 13.1  Project proposal due 
11  2/27 
Abstraction (contd.) and Symbolic Model Checking without BDDs
(
PDF
)


12  3/1 
More Abstraction; Notions of Simulation and Language Equivalence
(
PDF
)

McMillan paper, Ch. 11  HW 3 out 
13  3/6 
Compositional Reasoning and Symmetry; MuCalculus
(
PDF
)

MC Ch. 14, 12, 7  
14  3/8 
Pushdown Model Checking
(
PDF
)

S. Schwoon's thesis (Sec. 2.1  2.3, Ch. 3)  HW 3 due 
15  3/13 
Games and Verification
(
PDF
)

F. Mang's thesis  HW 4 out 
3/15  Class rescheduled to 3/17 from 12:30  2pm in Cory 299  
16  3/17 
Model Generation from Traces
(
PDF
)


Part II: Systems with NonBoolean State and Applications  
17  3/20 
Firstorder logic and SATBased Automated Theorem Proving
(
PDF1,
PDF2
)

S. Seshia thesis  
18  3/22 
More SATBased Automated Theorem Proving
(
PDF
)

HW 4 due; HW 5 out  
3/27  Spring recess  
3/29  Spring recess  Part II required readings below  
19  4/3  Interface Automata: Theory and Applications. Guest lecture by Arindam Chakrabarti. ( PDF )  [dAH01]  
20  4/5 
Software Verification I: Abstractionbased Model Checking.
Guest lecture by Prof. Rupak Majumdar.
(
PDF
)

SLAM (pdf), Bebop (pdf), Blast.  HW 5 and Project preliminary report due 
21  4/10 
Software Verification II: Executionbased Model Checking

VeriSoft (ps), CMC (pdf)  
22  4/12 
Software Verification III: Reasoning about Concurrency

Zing overview (pdf), [QRR04] (pdf), [FQ03] (ps)  HW 6 out 
23  4/17 
Model Checking RealTime Systems

[Alur97] (gzipped ps)  
4/19  Class cancelled (Sanjit travelling)  
24  4/24  Model Checking Hybrid Systems  [ACH+95]  HW 6 due 
25  4/26 
Hardware and SystemLevel Verification

[BD94] (pdf), [CB95] (pdf), CBMC (pdf)  
26  5/1 
Computational Logic and Security

[CJM00] (pdf, can skip Sec. 4.2, 4.3), [MMS97] (ps, can skip Sec. 4)  
5/3  Project presentations  I  Final project report due May 7th, 5 pm.  
5/8  Project presentations  II 