CMSC 838Z: Tools and Techniques for Software Dependability

Instructor Michael Hicks
CSI 2120 TuTh 3:30-4:45pm
Office Hours TuTh 10:00-11:00am AVW 4131

Syllabus / Schedule / Resources / Wiki

Jan 27

University closed.
Jan 29, Feb 2
Type Systems: Review
Type Systems, Luca Cardelli, Secs 1-3,5.
Also see Chapter  9 of Pierce's Types and Programming Languages (on reserve in the CS library), and Grossman's slides on universal types, and recursive and abstract types.
Project 1 due Feb 12.
Feb 5

No class.
Feb 9

Quantified Types in an Imperative Language, Dan Grossman. (Draft, do not distribute.)
Cyclone User's Manual
Cyclone: A Safe Dialect of C, Trevor Jim, Greg Morrisett, Dan Grossman, Michael Hicks, James Cheney, and Yanling Wang.
Cyclone example comparing universal and existential quantification.
Feb 12 Region-based Memory Management in Cyclone, Dan Grossman, Greg Morrisett, Trevor Jim, Michael Hicks, Yanling Wang, and James Cheney.
Safe and Flexible Memory Management in Cyclone, Mike Hicks, Greg Morrisett, Dan Grossman, and Trevor Jim. (optional)

Feb 17,19 CQual CQual User's Guide
Flow-insensitive Type Qualifiers, Jeffrey S. Foster, Robert Johnson, John Kodumal, and Alex Aiken. (Draft, do not distribute.)
Project 2 due Feb 27.
See Cardelli Sec 6 for a discussion of subtyping.
Sample derivation from class.
Feb 24
Flow-Sensitive Type Qualifiers
Jeffrey S. Foster, Tachio Terauchi, and Alex Aiken.

Feb 26 Race-free Java Types for Safe Locking, Cormac Flanagan and Martin Abadi.
Mar 2
Type-based race detection for Java, Cormac Flanagan and Stephen Freund.
A Parameterized Type System for Race-Free Java Programs,  Chandrasekhar Boyapati, Martin Rinard. (optional; improves on above system.)
Project 3 due March 12.
Mar 4 Daikon Dynamically discovering likely program invariants to support program evolution, Michael D. Ernst, Jake Cockrell, William G. Griswold, and David Notkin.
Invariant inference for static checking: An empirical evaluation, Jeremy W. Nimmer and Michael D. Ernst.
Start thinking about projects
Mar 9
Extended Static Checking, David L. Detlefs, K. Rustan M. Leino, Greg Nelson, and James B. Saxe.
Extended Static Checking for Java, Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, and Raymie Stata.
See also Hoare's seminal paper.
Mar 11
Verification Conditions.  See lecture notes by Necula; lectures 2-4 are useful, and lecture 3 is specifically on Verification Conditions. Project 4 due March 31.
Mar 16
Houdini, an Annotation Assistant for ESC/Java, Cormac Flanagan and K. Rustan M. Leino.
Annotation Inference for Modular Checkers, Cormac Flanagan, Rajeev Joshi, and K. Rustan M. Leino.

Mar 18
Simplification by Cooperating Decision Procedures, Greg Nelson and Derek C. Oppen.

Mar 23,25

Spring Break.
Mar 30 Vault
Enforcing High-level Protocols in Low-level Software, Robert DeLine and Manuel Fahndrich.
Adoption and Focus: Practical Linear Types for Imperative Programming, Manuel Fahndrich and Robert DeLine.
Final project proposal due.
Apr 1
Project discussions

Apr 6
Alias Types, Fred Smith and David Walker and Greg Morrisett.
Alias Types for Recursive Data Structures, David Walker and Greg Morrisett.
Relevant foundation for Vault and other flow-sensitive checkers (like CQual).

Slides courtesy of Dave Walker.
Apr 8
Verification by Model Checking, Chapter 3, Logic in Computer Science, Michael R. A. Huth and Mark D. Ryan.
SMV program demonstrating mutual exclusion.
Apr 13
Blast Lazy Abstraction, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Gregoire Sutre.

Apr 15,20
Twelf Formalization in a Logical Framework, Chapter 3, Computation and Deduction, Frank Pfenning.
You may wish to refer to Chapter 2 as well, for the specifics of the Mini-ML language being formalized.
Here are some supplementary slides.
Apr 20
Student Presentations
Tracking Pointers with Path and Context Sensitivity for Bug Detection in C Programs, V. Benjamin Livshits and Monica S. Lam [Mujtaba Ali]. Project 5 due May 11 (extra credit).
Apr 22
Abstract Types and the Dot
, Luca Cardelli, and Xavier Leroy [Mike Furr].
Type-Based Hot Swapping of Running Modules, Dominic Duggan [Iulian Neamtiu].

Apr 27
Mining Specifications,
Glenn Ammons, Rastislav Bodik, and James R. Larus [Rob Sherwood].

Type-Based Flow Analysis: From Polymorphic Subtyping to CFL-Reachability, Jakob Rehof and Manuel Fahndrich [Polyvios Pratikakis].

Apr 29
Points-to Analysis in Almost Linear Time, Bjarne Steensgaard [Jeff Blank].
A Calculus of Capabilities, Karl Cray, David Walker, and Greg Morrisett [Nikhil Swamy].

May 4
Project Presentations
[Nik Swamy], [Mujtaba Ali], [Mike Furr], [Iulian Neamtiu]

May 6
[Rob Sherwood], [Polyvios Pratikakis], [Jeff Blank].

May 11
Project 5 due.
May 17
Project Demos
Mike Furr - 2pm
Polyvios Pratikakis - 2:30pm
Nikhil Swamy - 3:00pm
Rob Sherwood - 3:30pm
Jeff Blank - 4pm

May 18
Project Demos
Iulian Neamtiu - 11:30am
Mujtaba Ali - 3pm

May 18 Final
Final project writeup due, 12:30pm.
Take-home exam distributed 12:30pm.
May 19

Final exam due, 12:30pm.