| 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
[Slides] |
| 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
[Slides] |
| 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
[Slides] |
| 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
[Slides] |
| 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
[Slides] |
| 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
[Slides] |
| 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
[Slides] |
| 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
[Slides] |
| 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
[Slides] |
| 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
[Slides] |
| 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
[Slides] |
| 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
- Software Model Checking,
R. Jhala, R. Majumdar, ACM Comput. Surveys, 41(4), 2009
- Formal Methods: Practice and Experience,
J. Woodcock, P. Larsen, J. Bicarregui, J. Fitzgerald, ACM Comput. Surveys, 41(4), 2009
- Automated Deduction for Verification,
N. Shankar, ACM Comput. Surveys, 41(4), 2009
- Proving Program Termination, B. Cook, A. Podelski, A. Rybalchenko, Comm. ACM, 54(5): 88-98, 2011
|
|
