The AMPS Seminar -- CS 7931 -- Spring 2009
Meetings : 2:00pm to 3:30pm in MEB 3105 on FRIDAYS
AMPS is to discuss papers that interest the Gauss group.
There should be sufficient
selections for students not in the Gauss group as well
(so that these can be read by, e.g.,
The following list comes from Fall 2008.
A few papers have already been discussed, and those will be in
small sf font.
``Evidence-Based Analysis and Inferring Preconditions for Bug Detection,'' by Brand, Buss, Sreedhar, ICSM 2007. Speaker must present key ideas, and also work with person presenting paper ``Flexbile
Pointer Analysis Using Assign-Fetch Graphs.''
- Buss, Brand, Sreedhar, and Edwards, ``Flexbile Pointer Analysis Using Assign-Fetch Graphs,'' SAC 2008.
- Boehm, ``Reordering Constraints for Pthread-Style Locks,'' PPoPP 200?.
- Krstic, ``Parameterized System Verification with Guard Strengthening and Parameter Abstraction,'' AVIS 2005.
- Godefroid, ``Compositional Dynamic Test Generation,'' POPL 2007.
- Flanagan, Freund, and Qadeer, ``Exploiting Purity for Atomicity,'' IEEE Trans on SW Engg, Apr 2005. (Read with the type and effect system for atomicity paper below.)
- Flanagan and Qadeer, ``A Type and Effect System for Atomicity,'' Flanagan and Qadeer.
- Reps, Horowitz, and Sagiv, ``Precise Interprocedural Dataflow Analysis via Graph Reachability,'' (a classic; forgot ref)
- Musuvathi and Qadeer,
``Fair Stateless Model Checking,'' PLDI 2008. Expecting someone to download, install, and demo Chess at the same time. The download/demo part is.
- Banerjee, Bliss, Ma, Petersen, ``A Theory of Data Race Detection,'' PADTAD 2006. (Read with following.)
- Banerjee, Bliss, Ma, Petersen, ``Unraveling Data Race Detection in the Intel Thread Checker,'' Intel report.
- Majumdar and Sen, ``Hbyrid Concolic Testing,'' Intl. Conf on SW Engg, 2007. (Read with other testing papers.)
- Salcianu and Rinard, ``Pointer and Escape Analysis for Multithreaded Programs,'' PPoPP 2001.
- Godefroid, Klarlund, and Sen, ``DART: Directed Automated Random Testing,'' PLDI 2005.
- Wang, Yang, Kahlon, and Gupta, ``Peephole Partial Order Reduction,'' TACAS 2008.
- Anand, Godefroid, and Tillmann, ``Demand-Driven Compositional Symbolic Execution,'' TACAS 2008.
- Hamon, de Moura, and Rushby, ``Automated Test Generation with SAL,'' SRI Tech Note, Jan 2005. Expecting SAL to be demoed.
- Elmas, Tasiran, and Qadeer, ``VYRD: VerifYing Concurrent Programs by Runtime Refinement-Violation Detection,'' PLDI 2005.
- D'Silva, Kroening, and Weissenbacher, ``A Survey of Automated Techniques for Formal Software Verification,'' IEEE Trans CAD, July 2008.
- Boehm, ``N2480: A Less Formal Explanation of the Proposed C++ Concurrency Memory Model,'' TR. These and other memory models for languages papers must be read together with Sutter's PRISM work.
This document was translated from LATEX by