Instructor: Cormac Flanagan
Seminar: Thursdays, 2:05-3:45pm
***New Room***: Software Engineering Lab, Engineering 2 Building, room 392 Office Hours: Tuesday 4:30-5:30pm, Thursdays 8:30-9:30am, or by appointmentOverview: This class is a graduate seminar on software engineering and programming languages. Students read technical papers and present class lectures. Students are particularly encouraged to present their own research. Guest lectures supplement the student presentations.
|
September 23 |
- Cormac Flanagan on Type Inference Against Races |
|
September 30 |
- Sung Kim on Semantic API Framework |
|
October 7 |
- Kai Pan on Link-based Change Impact Analysis |
|
October 14 |
- Luca de Alfaro |
|
October 21 |
- Kim Bruce on Fixing the meaning of Object-Oriented Languages |
|
October 28 |
- Jim Whitehead |
|
November 4 |
- Guozheng Ge on Automatic
Generation of Rule-based Software Configuration Management Systems Helpful background reading includes: Containment Modeling of Content Management Systems and Automatic Generation of Hypertext System Repositories, A Model Driven Approach |
|
November 11 |
- Holiday - no class |
|
November 18 |
- Marco Faella on Model Checking Quantitative Temporal Properties |
|
November 25 |
- Thanksgiving - no class |
|
December 2 |
- Ranjit Jhala from UC Berkeley on Permissive Interfaces (see abstract below). |
A modular program analysis considers components independently and provides succinct summaries for each component, which can be used when checking the rest of the system. Consider a system comprising of two components, a library and a client. A temporal summary, or interface, of the library specifies legal sequences of library calls. The interface is safe if no call sequence violates the library's internal invariants; the interface is permissive if it contains every such sequence. Modular program analysis requires full interfaces, which are both safe and permissive: the client does not cause errors in the library if and only if it makes only sequences of library calls that are allowed by the full interface of the library.
Previous interface-based methods have focused on safe interfaces, which may be too restrictive and thus reject good clients. We present an algorithm for automatically synthesizing software interfaces that are both safe and permissive. The algorithm generates interfaces as graphs whose vertices are labeled with predicates over the library's internal state, and whose edges are labeled with library calls. The interface state is refined incrementally until the full interface is constructed. In other words, the algorithm automatically synthesizes a typestate system for the library, against which any client can be checked for compatibility. We present an implementation of the algorithm which is based on the BLAST model checker, and we evaluate some case studies.