Date Topic Readings Presenter
Sep. 23 Symbolic Execution SELECT - a formal system for testing and debugging programs by symbolic execution, R. Boyer, B. Elspas, K. Levitt, Int. Conf. Reliable Software, 1975
Symbolic execution and program testing, J. King, Comm. ACM, 1976
Klee: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs, C. Cadar, D. Dunbar, D. Engler, OSDI 2008
Stefan Bucur
Sep. 30 Fuzz Testing An Empirical Study of the Reliability of UNIX Utilities, B.P. Miller, L. Fredriksen, and B. So, Comm. ACM, 1990
Automated Whitebox Fuzz Testing, P. Godefroid, M. Levin, D. Molnar, NDSS 2008
Radu Banabic
Oct. 7 Stateless Model Checking Model checking for programming languages using VeriSoft, P. Godefroid, POPL 1997
Dynamic partial-order reduction for model checking software, C. Flanagan, P. Godefroid, POPL 2005
Baris Kasikci
Oct. 14 Dynamic Test Generation DART: directed automated random testing, P. Godefroid, N. Klarlund, PLDI 2005
EXE: Automatically Generating Inputs of Death, C. Cadar, V. Ganesh, P. Pawlowski, D. Dill, D. Engler, CCS 2006
Peter Peresini
Oct. 21 Scalable Static Analysis Saturn: A Scalable Framework for Error Detection using Boolean Satisfiability, Y. Xie, A. Aiken, ACM Trans. Prog. Lang. Syst., 29(3), 2007
Calysto: scalable and precise extended static checking, D. Babic, ICSE 2008
Andrew Becker
Oct. 28 Predicate Abstraction Automatic predicate abstraction of C programs, T. Ball, R. Majumdar, T. Millstein, S. Rajamani, PLDI 2001
Thorough static analysis of device drivers, T. Ball et al., EUROSYS 2006
Daniel Lupei
Nov. 4 Concurrency Testing Finding and reproducing Heisenbugs in concurrent programs, M. Musuvathi, S. Qadeer, T. Ball, G. Basler, P. Nainar, and I. Neamtiu, OSDI 2008
Coverage guided systematic concurrency testing, C. Wang, M. Said, A. Gupta, ICSE 2010
Trevis Alleyne
Nov. 11 Performance Analysis Finding Latent Performance Bugs in Systems Implementations, C. Killian, K. Nagaraj, S. Pervez, R. Braud, J. Anderson, R. Jhala, FSE 2010
Diagnosing Performance Changes by Comparing Request Flows, R. Sambasivan et al., NSDI 2011
Yannis Klonatos
Nov. 18 Abstract Interpretation [Optional] Original paper: Abstract Interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, P. Cousot, R. Cousot, POPL 1977
Gentle introduction: Abstract Interpretation of Numerical Properties, A. Miné, PhD Thesis, Chapter 2, 2004
A static analyzer for large safety-critical software, B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, X. Rival, PLDI 2003
Etienne Kneuss
Nov. 25 Compositional Symbolic Execution Compositional Dynamic Test Generation, P. Godefroid, POPL 2007
Exploiting Program Dependencies for Scalable Multiple-path Symbolic Execution, R. Santelices, M. Harrold, ISSTA 2010
Jonas Wagner
Dec. 2 Symbolic Reasoning and Concrete Execution Symbolic Execution with Mixed Concrete-Symbolic Solving, C. Păsăreanu, N. Rungta, W. Visser, ISSTA 2011
Higher Order Test Generation, P. Godefroid, PLDI 2011
Andrii Vozniuk
Dec. 9 Practical Symbolic Execution S2E: A Platform for In-Vivo Multi-Path Analysis of Software Systems, V. Chipounov, V. Kuznetsov, G. Candea, ASPLOS 2011
Parallel Symbolic Execution for Automated Real-World Software Testing, S. Bucur, V. Ureche, C. Zamfir, G. Candea, EUROSYS 2011
Sergii Vozniuk
Dec. 16 From Tests to Proofs Proofs from Tests, N. Beckman, A. Nori, S. Rajamani, R. Simmons, S. Tetali, A. Thakur, IEEE Trans. Software Eng., 36(4): 495-508, 2009
[Optional] The Yogi Project: Software Property Checking via Static Analysis and Testing, A. Nori, S. Rajamani, S. Tetali, A. Thakur, TACAS 2009 (tool paper)
Compositional may-must program analysis: unleashing the power of alternation, P. Godefroid, A. Nori, S. Rajamani, S. Tetali, POPL 2010
Vova Kuznetsov
Dec. 23 Model Checking Distributed Systems Life, death, and the critical transition: Finding liveness bugs in systems code, C. Killian, J. Anderson, R. Jhala, A. Vahdat, NSDI 2007
MODIST: Transparent Model Checking of Unmodified Distributed Systems, J. Yang et al., NSDI 2009

Suggested Further Reading