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).
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 
FiniteState Model Checking  Introduction
(
PDF
)

MC Ch. 3  
7  2/12 
ExplicitState Model Checking
(
PDF
)

MC Ch. 9: 9.1, 9.2; SPIN Ch. 6, 8  
8  2/14 
More ExplicitState 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
(Makeup 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; MuCalculus
(
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 2945 class on 4/3, 11:30 am  1 pm in 405 Soda  
20  4/4 
Learning Algorithms in Model Checking: Abstraction and AssumeGuarantee Reasoning
(Guest lecture by Dr. Anubhav Gupta, Cadence Berkeley Labs) ( PDF ) 
Project preliminary report due by email 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 