The following schedule is tentative.
Electronic copies of the lecture notes used in class will be provided on this web page.
| Class | Lecture Number | Topic | Notes | ||||||||||||||||||||||||||||||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Jan
7 |
1 |
Overview, Motivation, and Outline | pdf(4up) |
||||||||||||||||||||||||||||||||||||||||||||
| 2 |
Propositional Logic |
prop-nat-ded-rules |
|||||||||||||||||||||||||||||||||||||||||||||
| Jan
14 |
3 |
Predicate
Logic |
pdf(4up) pred-nat-ded-rules |
||||||||||||||||||||||||||||||||||||||||||||
| 4 |
Introduction to Model Checking, LTL, Kripke structures, CTL | temp-logic-exercise |
|||||||||||||||||||||||||||||||||||||||||||||
| Jan
21 |
5 |
Symbolic
Model Verifier (SMV) Assignment #1 (model checking) handed out |
pdf(4up) echo1.smv echo2.smv echo3.smv therm1.smv therm2.smv therm3.smv therm4.smv therm5.smv interleaving1.smv interleaving2.smv |
||||||||||||||||||||||||||||||||||||||||||||
| Jan 26 | 6 |
Explicit CTL Model Checking |
|
||||||||||||||||||||||||||||||||||||||||||||
| Jan
28 |
7 |
Symbolic
CTL Model Checking |
pdf(4up) |
||||||||||||||||||||||||||||||||||||||||||||
| 8 |
Binary Decision Diagrams (BDDs) Project Discussion |
pdf(4up) | |||||||||||||||||||||||||||||||||||||||||||||
| Feb
4 |
9 |
Semantically
Configurable Model Checking Assignment #1 DUE |
pdf(4up) |
||||||||||||||||||||||||||||||||||||||||||||
| (Bryan) Klaus Havelund and
Tom Pressburger. Model Checking Java
Programs Using Java PathFinder International Journal on Software
Tools for Technology Transfer (STTT). Volume 2 Number 4. April 2000. (Mazen) Matthew B. Dwyer, George S. Avrunin, and James C. Corbett. Patterns in Propery Specification for Finite-State Verification. In Proceedings of the 21st International Conference on Software Engineering, May 1999 Stefan Edelkamp, Alberto Lluch Lafuente and Stefan Leue, Protocol Verification with Heuristic Search, Proc. AAAI Spring Symposium, AAAI, Stanford, March 2001 |
|
||||||||||||||||||||||||||||||||||||||||||||||
| Feb
11 |
(Ali R.) Gerard Holzmann,The Spin Model Checker, IEEE
Trans. on Software Engineering, Vol. 23, No. 5, May 1997, pp. 279-295. (Ruth) Paul Gastin and Pierre Moro, Minimal Counterexample Generation for SPIN, in Lecture Notes in Computer Science, LNCS 4595, August 2007, pp. 24-38. (Colleen) Jamieson M. Cobleigh, Lori A. Clarke, and Leon J. Osterweil, The Right Algorithm at the Right Time: Comparing Data Flow Analysis Algorithms for Finite State Verification. In Proceedings of the International Conference on Software Engineering, 2001. |
||||||||||||||||||||||||||||||||||||||||||||||
| Feb
16 |
READING
WEEK |
||||||||||||||||||||||||||||||||||||||||||||||
| (Ana) William Chan, Richard J. Anderson, Paul Beame, Steve
Burns,
Francesmary Modugno, David Notkin, and Jon D. Reese Model checking
large software specifications, IEEE Transactions on Software
Engineering, 1998. (Ramanan) Baoqiu Cui, Yifei Dong, Xiaoqun Du, K. Narayan Kumar, C. R. Ramakrishnan, I. V. Ramakrishnan, Abhik Roychoudhury, Scott A. Smolka, David S. Warren, Logic programming and model checking, In Proceedings of PLILP/ALP, LNCS 1490. |
|||||||||||||||||||||||||||||||||||||||||||||||
| Feb
25 |
(Mina)
Felix Sheng-Ho Chang and Daniel Jackson, Symbolic Model Checking
of Declarative Relational Models, In Proceedings of the 28th
International Conference on Software Engineering (ICSE), 2006. (Tejas) Robert B. Jones, John W. O'Leary, Carl-Johan H. Seger, Mark D. Aagaard, and Thomas F. Melham Practical Formal Verification in Microprocessor Design, IEEE Design and Test, 2001. |
||||||||||||||||||||||||||||||||||||||||||||||
| No Lecture | |||||||||||||||||||||||||||||||||||||||||||||||
| Mar
4 |
No Lecture |
||||||||||||||||||||||||||||||||||||||||||||||
| 10 |
Alloy Assignment #2 (model finding) handed out |
pdf(4up) quick reference |
|||||||||||||||||||||||||||||||||||||||||||||
| Mar
11 |
11 |
Alloy (cont.) | pdf(4up) grandpa.als addressBook.als |
||||||||||||||||||||||||||||||||||||||||||||
|
GTC.pdf |
||||||||||||||||||||||||||||||||||||||||||||||
| Mar
18 |
12 |
Abstraction
and Compositional Verification |
pdf(4up) |
||||||||||||||||||||||||||||||||||||||||||||
| (Jiewen) Satyaki Das, David L. Dill,
Seungjoon Park, Experience with
Predicate Abstraction CAV 1999. (Ali N.) Bharadwaj, Ramesh and Constance L. Heitmeyer, Model Checking Complete Requirements Specifications Using Abstraction Automated Software Engineering, Vol 6, No. 1, pp. 37-68, January 1999, Kluwer Academic Publishers |
|||||||||||||||||||||||||||||||||||||||||||||||
| Mar
25 |
(Zihon) Jerry R. Burch and David L. Dill,
Automatic
Verification of Pipelined Microprocessor Control, in Proceedings of Computer Aided
Verification, LNCS 818, 1994. (Eugene) Greg Dennis, Felix Sheng-Ho Chang, and Daniel Jackson, Modular Verification of Code with SAT, In Proceedings of International Symposium on Software Testing and Analysis, 2006. (Tariq) Yuan Yu, Panagiotis Manolios, Leslie Lamport, Model Checking TLA+ Specifications. In Proceedings of CHARME 1999. |
||||||||||||||||||||||||||||||||||||||||||||||
| Mar
27 |
Assignment #2 Due at 4:00 PM |
||||||||||||||||||||||||||||||||||||||||||||||
| Mar
30 |
No Lecture |
||||||||||||||||||||||||||||||||||||||||||||||
| Apr
1 |
Paper Presentation: (Hang) Patrice Godefroid, Pierre Wolper, A Partial Approach to Model Checking, Information and Computation, 1994. Project Presentation: (Hang, Zihon) Sliding Window Protocol using SPIN Course Critiques |
||||||||||||||||||||||||||||||||||||||||||||||
| Apr
6 |
10:00 AM 10:30 AM 11:00 AM 11:30 AM |
Project Presentations - location TBA (Ana, Bryan) Ground Traffic Control System using Java Pathfinder (Ali R., Tejas) Ground Traffic Control System using SPIN (Mina, Jiewen) Ground Traffic Control System using Murø (Tariq, Ram) Unmanned Vehicle Control using TLC |
|||||||||||||||||||||||||||||||||||||||||||||
| Apr
7 |
2:00 PM 2:30 PM 3:00 PM 3:30 PM |
Project Presentations - location TBA (Mazen) Ground Traffic Control System using LTSA (Colleen, Ruth) Light Control System using SPIN (Ali N.) Ground Traffic Control System using SCR* (Eugene) Cruise Control using SCR* |
|||||||||||||||||||||||||||||||||||||||||||||
| Apr 8 (Wed) | Project Reports DUE by 5pm | ||||||||||||||||||||||||||||||||||||||||||||||