CSE 291: Software Reliability Methods

Spring Quarter, 2006

General information

Meeting times and location: T-Th 9:30-11:00, location: HSS 1138
Instructors:
- Ingolf Krueger (email: ikrueger at cs, Office hours: TBD)
- Ranjit Jhala (email: rjhala at cs, Office hours: TBD)
- Sorin Lerner (email: lerner at cs, Office hours: TBD)
Course syllabus and course topics
Class mailing list: cse291-a "at" cs.ucsd.edu
- to subscribe send email to cse291-a-request "at" cs.ucsd.edu with the command "subscribe" in the body.

Course Readings

Course project

Information about the project will be available here

Schedule (ever evolving)

Week 1	Tu 04/04	Introduction
Week 1	Th 04/06	Introduction (continued) Slides from Sorin's presentation: [ppt]
Week 2	Tu 04/11	Scheduling of paper presentations
Week 2	Th 04/13	Modelling
Week 3	Tu 04/18	E.W. Dijkstra, Cooperating Sequential Processes. Cooperating Sequential Processes. EWD 123. Presented by Max (B 4). C. A. R. Hoare, An Axiomatic Basis for Computer Programming. Communications of the ACM 12(10): 576-580 (1969). Presented by Zach (B 7).
Week 3	Th 04/20	Jayadev Misra, A logic for Concurrent Programming (in two parts): Safety and Progress, Journal of Computer and Software Engineering, Vol.3, No.2, pp 239-300, 1995. Presented by Richard (MC 20). Manfred Broy, Ingolf Krueger, Interaction Interfaces - Towards a Scientific Foundation of a Methodological Usage of Message Sequence Charts, ICFEM 1998. Presented by Zach. (MC 3)
Week 4	Tu 04/25	Markus Kaltenbach, Jayadev Misra, A Theory of Hints in Model Checking, in Formal Methods at the Crossroads: From Panacea to Foundational Support, ed. Bernhard K. Aichernig and Tom Maibaum, LNCS 2757, pp 423-438, Springer-Verlag, 2003. Presented by Chris (MC 18). Jayadev Misra, A Simple, Object-based View of Multiprogramming, Formal Methods in System Design, Vol. 20, No. 1, January 2002. Presented by Jan (MC 19).
Week 4	Th 04/27	Patrice Godefroid, Doron Peled and Mark G. Staskauskas, Using Partial-Order Methods in the Formal Validation of Industrial Concurrent rograms. ISSTA 1996, 261-269. Presented by Max (MC 11). Doron Peled, Amir Pnueli, Proving Partial Order Properties. TCS 126(2): 143-182 (1994). Presented by Monica (MC 22).
Week 5	Tu 05/02	J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking 10²⁰ states and beyond. Information and Computation, 98(2):142--170, June 1992. Presented by Vina (MC 5). Kenneth L. McMillan, Applications of Craig Interpolation to Model Checking, TACAS 05. Presented by Monica (MC 29).
Week 5	Th 05/04	Patrice Godefroid, Sarfraz Khurshid: Exploring Very Large State Spaces Using Genetic Algorithms, J.-P. Katoen and P. Stevens (Eds.): TACAS 2002, LNCS 2280, pp. 266.280, 2002. Presented by John (MC 10). SMV. Kenneth L. McMillan: Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking, CAV 1998. Presented by Jessica (MC 32).
Week 6	Tu 05/09	Thomas Ball and Sriram Rajamani. Bebop: A Path-sensitive Interprocedural Dataflow Engine. Presented by Jessica (PA 5). P. Cousot and R. Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, POPL 1977. Presented by Max and Vina (PA 1). P. Cousot and R. Cousot, Systematic design of program analysis frameworks, POPL 1979. Presented by Max and Vina (PA 2).
Week 6	Th 05/11	N. Sharygina and D. Peled. A Combined Testing and Verification Approach for Software Reliability. In Formal Methods for Increasing Software Productivity, International Symposium of Formal Methods Europe, pages 611-628, 2001. Presented by Chris (T 9). Stefan Savage, Michael Burrows, Greg Nelson, Patrick Sobalvarro and Thomas Anderson, Eraser: a dynamic data race detector for multithreaded programs, TOCS Nov 1997. Presented by John (PA 9).
Week 7	Tu 05/16	Westley Weimer and George C. Necula, Finding and Preventing Run-time Error Handling Mistakes, OOPSLA 2004. Presented by Jennifer (PA 11). Carl Gould, Zhendong Su, and Premkumar Devanbu, Static Checking of Dynamically Generated Queries in Database Applications. ICSE 2005. Presented by Jennifer (PA 6).
Week 7	Th 05/18	PET, presented by Vina. Need to pick the right paper of these three to read: Elsa L. Gunter, Doron Peled, Using Functional Languages in Formal Methods: The PET System. PDPTA 2000: 2981-2986. Presented by Vina (T 3). Elsa L. Gunter, Robert P. Kurshan, Doron Peled, PET: An Interactive Software Testing Tool. CAV 2000: 552-556. Presented by Vina (T 4). Elsa L. Gunter, Doron Peled, Path Exploration Tool. TACAS 1999: 405-419. Presented by Vina (T 5). Anders Ek, Jens Grabowski, Dieter Hogrefe, Richard Jerome, Beat Koch, Michael Schmitt II: Towards the industrial use of validation techniques and automatic test generation methods for SDL specifications. SDL Forum 1997: 245-260. Presented by Brian (T 2).
Week 8	Tu 05/23	Jeffrey S. Foster, Tachio Terauchi, and Alex Aiken, Flow-Sensitive Type Qualifiers, PLDI 02. Presented by Brian (PA 8). Robert O'Callahan, Daniel Jackson: Lackwit: A Program Understanding Tool Based on Type Inference. ICSE 1997: 338-348. Presented by Jessica (TS 15).
Week 8	Th 05/25	Alexander Aiken, Introduction to Set Constraint-Based Program Analysis. Science of Computer Programming 35(2): 79-111 (1999). Presented by Jan (TS 3). Cormac Flanagan, Stephen N. Freund, Type-based race detection for Java. PLDI 2000: 219-232. Presented by Monica and Richard (TS 12). Cormac Flanagan and Shaz Qadeer, A Type and Effect System for Atomicity, PLDI 03. Presented by Monica and Richard (TS 13).
Week 9	Tu 05/30	Philip Wadler, Linear types can change the world!, in M. Broy and C. Jones, editors, Programming Concepts and Methods, Sea of Galilee, Israel, April 1990. North Holland, Amsterdam, 1990. Presented by Richard (TS 4). Philip Wadler, A taste of linear logic, Springer Verlag LNCS 802, 1993. Presented by Richard (TS 5). Dan Grossman, Greg Morrisett, Trevor Jim, Florham Park, Michael Hicks, Yanling Wang, James Cheney, Region-Based Memory Management in Cyclone, PLDI 02. Presented by Jan (TS 10)
Week 9	Th 06/01	Flanagan, Leino, Lillibridge, Nelson, Saxe, State, Extended Static Checking for Java, PLDI 02. Presented by Chris (ATP 3) T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre, Lazy Abstraction, POPL 02. Presented by Zach (ATP 5)
Week 10	Tu 06/06	George Necula and Peter Lee, Proof-Carrying Code. POPL 1996. Presented by Jennifer (ATP 1). Patrice Godefroid, Nils Klarlund, Koushik Sen, DART: Directed Automated Random Testing, PLDI 2005. Presented by John (ATP 9).
Week 10	Th 06/08	Lerner, Millstein, Rice, Chambers, Automated Soundness Proofs for Dataflow Analyses and Transformations via Local Rules, POPL 05. Presented by Brian (ATP 8).