UC Santa Cruz

Apr 2
- Discussion of possible topics
  - concurrency & geometry
  - popl 08 papers
  - model checking
  - et cetera

Apr 8: Geometry and Concurrency
- Geometry and Concurrency: A User's Guide. Eric Goubault. Mathematical Structures in Computer Science (2000).
- Learning from Mistakes - A Comprehensive Study on Real World Concurrency Bug Characteristics. Lu, Park, Seo, Zhou. ASPLOS 2008.

Apr 15: Model Checking: Past and Present
- Design and synthesis of synchronization skeletons using branching time temporal logic. Clarke and Emerson. LNCS Logic of Programs, 1982.
- Model Checking Programs. Visser, Havelund, Brat, Park, Lerda. International Journal on Automated Software Engineering 2003.

Apr 22: Concurrency and Version Control
- The Theory of Patches. David Roundy. Darcs Manual 2.0.0 (+ 29 patches), retrieved 2008.
- A Principled Approach to Version Control. Loh, Swierstra, Leijen. Draft, 2007.
- Generalized File System Dependencies. C Frost, M Mammarella, E. Kohler, A de los Reyes, S Hovsepian, A Matsuoka, L Zhang. SOSP 2007.

Apr 29: Abstract Interpretation
- Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation Of Fixpoints. P Cousot, R Cousot. POPL 1977.
- Optional. Abstract Interpretation. P Cousot. ACM Computing Surveys, 1996.
- Optional. Reﬁning Model Checking by Abstract Interpretation. P Cousot, R Cousot. Automated Software Engineering, 6, 69–95 (1999).
- Reference. Abstract Interpretation slides. G Necula. CS263 (2007).
- Reference. Denotational Semantics slides. G Necula. CS263 (2007).

May 6: Abstraction and Refinement for Model Checking
- Model Checking and Abstraction. E Clarke, O Grumberg, D Long. TOPLAS 1994.
- Counterexample-Guided Abstraction Refinement. E Clarke, O Grumberg, S Jha, Y Lu, H Veith. CAV 2000.
- Optional. Automatic Abstraction without Counterexamples. K McMillan, N Amla. TACAS 2003.
- Reference. Lecture notes on omega-automata, buchi/muller automata, L-processes. Eduard Cerny. 1999.

May 13: Random Testing Techniques
- DART: Directed Automated Random Testing. P Godefroid, N Klarlund, K Sen. PLDI 2005.
- Compositional Dynamic Test Generation. P Godefroid. POPL 2007.

May 20: Formalization / Java Model Checking
- Coq/Velodrome writeup for workshop
- Formalization and Verification of a Mail Server in Coq. R Affeldt, N Kobayashi. International Symposium on Software Security, 2002.
- A Coq Library for Verification of Concurrent Programs. R Affeldt, N Kobayashi. 4th International Workshop on Logical Frameworks and Meta-Languages (LFM 2004).
- Model-Checking Multi-Threaded Distributed Java Programs. S Stoller. International Journal on Software Tools for Technology Transfer, 2000.
May 27: Partial-Order Reduction
- Formal Verification of a Partial-Order Reduction Technique for Model Checking. C Chou, D Peled. Journal of Automated Reasoning, 1999.
- Distributed Dynamic Partial Order Reduction based Verification of Threaded Software. Y Yang, X Chen, G Gopalakrishnan, RM Kirby. Workshop on Model Checking Software (SPIN 2007).
- (Optional) State Space Reduction Using Partial Order Techniques. EM Clarke, O Grumberg, M Minea, D Peled. International Journal on Software Tools for Technology Transfer, 1999.
June 5 (Thursday): PLDI papers: A Potpourri on Concurrency, Model Checking, Transactional Memory
- Deriving Linearizable Fine-Grained Concurrent Objects. Martin Vechev, Eran Yahav. PLDI 2008.
- Model Checking Transactional Memories. R Guerraoui, T Henzinger, V Singh. PLDI 2008.
- A Race and Transaction-Aware Runtime for Java Tayfun Elmas, Serdar Tasiran, Shaz Qadeer. PLDI 2007.