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.
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
List of Papers
Wednesday, 1st June
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
The paper discusses several now standard protocol security models. The paper has 2287 citations, according to Google Scholar.
Wednesday, 13th April
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
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
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
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
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
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.