Reading Group Fall 2006
From PROLANGS Wiki
Prolangs Reading Group
Fall 2006
Thursdays, 1:30pm-3:30pm, CoRE B
Information
If you have any questions regarding this light seminar, please contact Prof. Ryder (ryder@cs) by email; our organizational meeting will be on Thursday, January 19, 2006 at 1:30pm.
Papers
Schedule
- Sept 7
- Introduction
- Sept 14
- Cancelled
- Sept 21
- Presenter: Chen Fu
- Paper: Compiler and runtime support for efficient software transactional memory
- Slides: Software Transaction Memory Introduction
- Sept 28
- Guest Speaker: Marsha Chechik (University of Toronto): Supporting Construction, Analysis and Understanding of Software Models
- Abstract:
Software systems of today are pervasive, increasingly complex, and error prone. Software bugs lead to a loss of productivity, denial of service, and security breaches, cost millions of dollars to the economy, and sometimes cause a loss of human life. It is clear that testing alone is not sufficient to improve our confidence in these systems and must be supplemented by more sophisticated analysis techniques.
In the talk, I will discuss several approaches aimed at automated reasoning about software artifacts. The first of these is YASM -- a software model-checker that reasons about models automatically extracted directly from C code. Unlike similar approaches, it is well suited for both verification and bug finding. Furthermore, YASM can check safety (i.e., assertion violations) and liveness (i.e., non-termination) properties. The current research prototype can handle programs which are a few thousand lines of code, and has been successfully applied to analyzing device drivers, parts of Linux filesystem, and parts of OpenSSH.
In the second part of the talk, I give a general overview of our activities in techniques for creating and understanding software models. In particular, I will describe our work on TLQSolver -- a model-exploration tool that uses model-checking technology to discover temporal logic properties of a design.
- Slides:
- Oct 5
- Moved to Oct 19
- Oct 12
- Cancelled
- Oct 19
- Presenter: Kelly Winters
- Paper: J. Anvik, L. Hiew, G. C. Murphy, Who Should Fix This Bug?, ICSE 2006.
- Slides: pdf
- Oct 26
- Presenter: Xiaoxia Ren
- Paper: B. Baudry, F. Fleurey, Y. Traon, Improving test suites for efficient fault localization, ICSE 2006.
- Slides: pdf
- Nov 2
- Presenter: Weilei Zhang
- Paper: Berger, Zorn, DieHard, Probabilistic memory safety for unsafe languages, PLDI 2006.
- Slides:
- Nov 9:
- Cancelled
- Nov 16:
- Guest Speaker: Anindya Banerjee (Kansas State University): Information Flow, Modularity, and Declassification
- Abstract:
We give, via a relational Hoare-like logic, the specification of an interprocedural and flow sensitive (but termination insensitive) information flow analysis for heap-manipulating programs. Pointer aliasing is ubiquitous in such programs, and can potentially leak confidential information. Thus the logic employs agreement assertions to describe the noninterference property that formalizes confidentiality, and employs region assertions to describe possible aliasing. Programmer assertions, in the style of JML, are also allowed, thereby permitting a more fine-grained specification of information flow policy. The logic supports local reasoning about state in the style of separation logic.
In the second, more speculative part of the talk, we show how the logic can be used to formalize some recent proposals for declassification. We also show limitations of the logic and consider how abstract interpretation techniques may be used to calculate the amount of information released by a security policy.
Parts of this work are joint with Torben Amtoft, Sruthi Bandhakavi, Roberto Giacobazzi, Isabella Mastroeni and David Naumann.
- Reading: T. Amtoft, S. Bandhakavi, and A. Banerjee, "A logic for information flow in object-oriented programs", POPL 2006.
- Slides:
- Nov 23:
- Cancelled
- Nov 30
- Presenter: Bruno Dufour
- Paper: X. Zhuang, M. J. Serrano, H. W. Cain and J. Choi, Accurate, efficient, and adaptive calling context profiling, PLDI'06.
- Slides:
- Dec 7
- Presenter: Ophelia Chesley
- Paper: Brian Hackett, Manuvir Das, Daniel Wang, Zhe Yang, Modular Checking for Buffer Overflows in the Large, ICSE'06.
- Slides:
