During the course you will read the three research papers listed
as required reading below. These papers form part of the examinable material for the
You are expected to study these papers in your own time. There will be one tutorial slot devoted to discussing each paper.
Below you will also find a list of recommended reading. You
are strongly encouraged to read these papers: their content will broaden your grasp of the topics studied during the course. However, they are not examinable.
A pdf of each paper is available for download.
Advice on Studying Papers
Take a look at this short paper on How to Read a Paper.
This paper suggests an effective scheme for quickly getting to grips with a paper. You may find this useful when reading papers for this course. However, if you do follow this advice then consider limiting your "third pass": the paper suggests that this may take 4-5 hours per paper, which is a bit much for this course.
You are strongly encouraged to study these papers collaboratively,
with colleagues on the course.
- Cristian Cadar, Vijay Ganesh, Peter M. Pawlowski, David L. Dill, Dawson R. Engler: EXE: automatically generating inputs of death. ACM Conference on Computer and Communications Security 2006: 322-335. Download PDF.
- Madanlal Musuvathi, Shaz Qadeer, Thomas Ball, Gérard Basler, Piramanayagam Arumuga Nainar, Iulian Neamtiu: Finding and Reproducing Heisenbugs in Concurrent Programs. OSDI 2008: 267-280. Download PDF.
- Xi Wang, Nickolai Zeldovich, M. Frans Kaashoek, Armando Solar-Lezama: Towards optimization-safe systems: analyzing the impact of undefined behavior. SOSP 2013: 260-275. Download PDF.
- Topic: Static Program Verification. Michael Barnett, K. Rustan M. Leino: Weakest-precondition of unstructured programs. PASTE 2005: 82-87. Download PDF.
- Topic: Dynamic Symbolic Execution. Cristian Cadar, Daniel Dunbar, Dawson R. Engler: KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. OSDI 2008: 209-224. Download PDF.
- Topic: Dynamic Symbolic Execution. Peter Boonstoppel, Cristian Cadar, Dawson R. Engler: RWSet: Attacking Path Explosion in Constrained-Based Test Generation. TACAS 2008: 351-366. Download PDF.
- Topic: Invariant Generation. Cormac Flanagan, K. Rustan M. Leino: Houdini, an Annotation Assistant for ESC/Java. FME 2001: 500-517. Download PDF.
- Topic: Compiler Testing. Vu Le, Mehrdad Afshari, Zhendong Su: Compiler validation via equivalence modulo inputs. PLDI 2014. Download PDF.
- Topic: Compiler Testing. Christopher Lidbury, Andrei Lascu, Nathan Chong, Alastair F. Donaldson: Many-core compiler fuzzing. PLDI 2015. Download PDF.
- Topic: The Lockset Algorithm. Stefan Savage, Michael Burrows, Greg Nelson, Patrick Sobalvarro, Thomas E. Anderson: Eraser: A Dynamic Data Race Detector for Multithreaded Programs. ACM Trans. Comput. Syst. 15(4): 391-411. Download PDF.
- Topic: Stack Canaries. Crispan Cowan, Calton Pu, Dave Maier, Jonathan Walpole, Peat Bakke, Steve Beattie, Aaron Grier, Perry Wagle, Qian Zhang, Heather Hinton: StackGuard: Automatic Adaptive Detection and Prevention of Buffer-Overflow Attacks. USENIX Security Symposium, 1998. Download PDF.
- Topic: Safe C Compilers. Richard W. M. Jones, Paul H. J. Kelly: Backwards-Compatible Bounds Checking for Arrays and Pointers in C Programs. AADEBUG 1997: 13-26. Download PDF.
- Topic: Safe C Compilers. Olatunji Ruwase, Monica S. Lam: A Practical Dynamic Buffer Overflow Detector. NDSS 2004. Download PDF.