About the Group

The goal of the reading group is to deepen understanding of the most influential papers that shaped software security, verification, and quality in general. The group will try to develop deeper understanding of technical contributions of each paper, their impact on subsequent work, as well as to learn as much as possible about different exposition and writing styles.

You can subscribe to the mailing list (or digests) here. Please feel free to use the mailing list for the following:

• Discussing the papers, both before and after the meetings
• Asking for help if you don't understand some aspects of the paper. The more prepared everyone is before the meeting, the more everyone will benefit from the meetings.
• Suggesting papers for the future meetings

The group is moderated and unsolicited advertising will not be tolerated.

Where and When

Seminal Papers Reading Group meets every Wednesday in Soda 373, 10:00am. The room is reserved till 11:30am.

Papers will be announced each Wednesday (for the following Wednesday) on this page and on the mailing list.

Prerequisites

Please read the papers if you want to attend. The majority of papers that are on the short list are sufficiently complex that you won't get much out of just listening to other people discussing stuff you don't understand. Unprepared people slow everyone down, and end up wasting everyone's time.

List of Papers

2011

---

Wednesday, 1st June

• Rajeev Alur and David Dill: The theory of timed automata

The paper presents the formal foundations (timed automata) of real-time and cyber-physical systems. It triggered a flood of follow-up work. The paper has 4419 citations, according to Google Scholar.

Wednesday, 27th April

• Danny Dolev, Andrew C. Yao: On the security of public key protocols

The paper discusses several now standard protocol security models. The paper has 2287 citations, according to Google Scholar.

Wednesday, 13th April

• Robert W. Floyd: Assigning Meanings to Programs
• C. A. R. Hoare: An Axiomatic Basis for Computer Programming

These two papers are often cited together, so it makes sense to read them together . The first paper has 2062 and the second 4041 citations, according to Google Scholar. These two papers have shaped 40 years of software verification and formal analysis.

Wednesday, 6th April

• Jeanne Ferrante, Karl J. Ottenstein, Joe D. Warren: The program dependence graph and its use in optimization

The paper introduces program dependence graphs, that make both the data and control dependencies explicit, and triggered a flood of work on intermediate forms for representing programs. It has 1664 citations, according to Google Scholar. A longer version of this paper was published in TOPLAS. Note: This paper was chosen by the reading group.

Wednesday, 30th March

• Randal E. Bryant: Graph-Based Algorithms for Boolean Function Manipulation

The paper introduces Binary Decision Diagrams (BDDs), a simple, but powerful, data structure for representing Boolean functions. BDDs have played a major role in the development of symbolic model checking, as they can be used to encode sets of states by using characteristic functions describing the elements of a set. Many other variants of decision diagrams have been developed over time. According to Google Scholar, the paper has been cited 7263 times. Another related great paper to read is R.E. Bryant: On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Application to Integer Multiplication. This paper discusses the computational complexity of BDDs and is great for understanding when and how to use BDDs. This paper has 552 citations, and is optional.

Wednesday, 16th March

• Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill and L.J. Hwang: Symbolic model checking: 10²⁰ States and beyond.

This is an early symbolic model checking paper and has 2511 citations according to Google Scholar. Clarke, Emerson and Sifakis received the 2007 Turing award for their contributions to model checking.

Wednesday, 9th March

• Leslie Lamport: Time, clocks, and the ordering of events in a distributed system.

The paper discusses ordering of events in distributed systems, presents a synchronization algorithm, introduces the happens-before relation, and proves a bound on how out of sync distributed processes can be, all in a bit more than six pages. The proposed algorithm is the basis for static race detection algorithms, the happens-before relation influenced later work on partial-order reduction and bounded model checking of concurrent programs, and the synchronization stuff influenced a lot of work in the distributed systems community. The paper has 6294 citations, according to Google Scholar.

Wednesday, 23rd February

• Patrick Cousot and Radhia Cousot: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints.

This paper shaped the next three and a half decades of research on static analysis. All the key concepts (abstract interpretation, widening, narrowing, ...) have their origins in this paper. According to Google Scholar, the paper has 4035 citations. This is not an easy paper to read. It helps to know a little bit of lattice theory when reading it. B. A. Davey and H. A. Priestley wrote a nice readable book on lattice theory, entitled Introduction to Lattices and Order. The slides from Cousot's course at MIT are also helpful.