Date
|
Topic
|
Readings
|
Notes
|
Jan 27
|
|
|
University closed.
|
Jan 29, Feb 2
|
Overview
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
|
Cyclone
|
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
|
ESC/Java
|
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
|
Simplify
|
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
|
SMV
|
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
Notation, 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
|
Review |
|
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.
|