CSE-655: Seminar in Languages

Preliminary List of Papers:

• Dataflow Analysis: Sample Analyses:
  • Reps, Horowitz and Sagiv, Precise Interprocedural Flow Analysis via Graph Reachability, POPL'95.
  • Intraprocedural Shape analysis (section 2.6 of Nileson, Nielson and Hankin text).

• Dataflow Analysis: Algorithms: Chapter 6 of Bielson, Nielson and Hankin text.

• Information-Flow Properties:
  • Andrew Myers, JFlow: Practical Mostly-Static Information Flow Control, POPL'99. See Myers' publications page for this paper.
  • Zdancewic, Zheng, Nystrom and Myers, Untrusted Hosts and Confidentiality: Secure Program Partitioning, SOSP'01. See Myers' publications page for this paper.
  • Myers and Liskov, Protecting Privacy using the Decentralized Label Model, ACM TOSEM, Oct 2000. See Myers' publications page for this paper.

• Temporal Properties of Pushdown Systems:
  • Finkel, Willems and Wolper, A direct symbolic approach to model checking pushdown systems, Infinity'97, ENTCS'97, vol 9.
  • Esparza, Schwoon, et al, Efficient Model checking for Pushdown Systems, CAV 2000, 2001.
  • SLAM @ Microsoft: Realistic software verification project at MSR. See SLAM Home Page for related papers.

• Control Flow Analysis of Software:
  • Lie, Chou, Engler and Dill, A Simple Method for Extracting Models from Protocol Code, ISCA 2001.
  • Wagner, Foster, Brewer and Aiken, A first step towards automated detection of buffer overrun vulnerabilities, Network and Dist. System Security Symp. 2000.
  • Wagner and Dean, Intrusion Detection via Static Analysis, 2001 Oakland conf. (IEEE Symposium on Security and Privacy).