Program Analysis

Overview
- Basic Program Analysis
- Slides
  - Mayur Naik's lecture Videos on "Software Testing and Analysis"
  - Mary Jean Harrold's slides (under the "Topic" column) on program analysis including data/control dependency, slicing, etc.
  - Wei Le's slides on program analysis (Note that the course schedule page doesn't list the symbolic execution slides 6.DART.ppt and 6.SymbolicExecution.pdf but these two slides are available in the root directly listing)
  - Xiangyu Zhang's slides on program analysis and Slides onSystems and Software Security
  - Işıl Dillig. A Gentle Introduction to Program Analysis. Talk slides at the Programming Languages Mentoring Workshop 2014.
- Need to master the following basic concepts and their differences and relationships
  - Data/Control Dependency (together named as Program/System Dependency) vs.
  - Information Flow vs.
  - Program Slicing vs.
  - Symbolic Execution
  - Dynamic Symbolic Execution (e.g., Pex, SAGE) vs.
  - KLEE Symbolic Execution
  - Modular Verification (e.g., Boogie based on which are Spec# for C# (see Tutorial), SMACK+Corral for C) vs.
  - Abstract Interpretation (e.g., Code Contracts)
  - Readings
    - Mary Jean Harrold, Gregg Rothermel, Alex Orso. Representation and Analysis of Software.
    - Anders Møller and Michael I. Schwartzbach. Static Program Analysis (Lecture Notes).
- Illinois PL-FM-SE reading lists for qualification exams
- General Software Verification
  - Vijay D’Silva, Daniel Kroening, and Georg Weissenbacher. A Survey of Automated Techniques for Formal Software Veriﬁcation. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. 2008.
  - Wolfgang Wogerer. A Survey of Static Program Analysis Techniques. 2005.
- Analysis Soundness (Soundness Website)
  - Benjamin Livshits, Manu Sridharan, Yannis Smaragdakis, Ondřej Lhoták, J. Nelson Amaral, Bor-Yuh Evan Chang, Samuel Z. Guyer, Uday P. Khedker, Anders Møller, and Dimitrios Vardoulakis. In defense of soundiness: a manifesto. CACM 2015.
  - Yannis Smaragdakis and Christoph Csallner. Combining static and dynamic reasoning for bug detection. TAP 2007.
- Abstract Interpretation
- Online video on "Abstract Interpretation: Introduction"
  - Abstract Interpretation slides by Patrick Cousot
- Slides and notes from Patrick Cousot's course
- Slides on "Static Program Analysis using Abstract Interpretation"
- Notes on Abstract Interpretation
  - Patrick Cousot and Radhia Cousot. Abstract interpretation: past, present and future. CSL-LICS 2014.
  - David A. Schmidt. Data Flow Analysis is Model Checking of Abstract Interpretations. POPL 1998.
  - David A. Schmidt, Bernhard Steffen. Program Analysis as Model Checking of Abstract Interpretations. SAS 1998.
- Automated Deduction
  - Clark Barrett and Cesare Tinelli. Satisfiability Modulo Theories. Chapter on Satisfiability Modulo Theories. In E. Clarke and T. Henzinger and H. Veith editors, Handbook on Model Checking. Springer, 2014.
  - Nikolaj Bjørner and Leonardo de Moura. Applications of SMT solvers to Program Veriﬁcation. Rough notes for SSFT 2014 Prepared as part of a forthcoming revision of Daniel Kroening and Ofer Strichman’s book on Decision Procedures. 2014.
  - Willem Visser, Nikolaj Bjørner, and Natarajan Shankar. Software engineering and automated deduction. In FOSE 2014.
  - Clark Barrett, Daniel Kroening and Tom Melham. Problem Solving for the 21st Century: Efficient Solvers for Satisfiability Modulo Theories. Tech Report 2014.
  - Leonardo de Moura and Nikolaj Bjorner. Satisfiability Modulo Theories: Introduction and Applications. Communications of the ACM, vol. 54, no. 9, 2011.
  - Natarajan Shankar. Automated Deduction for Veriﬁcation. ACM Comput. Surv. 2009.
  - Clark Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. Satisfiability Modulo Theories. Handbook of Satisfiability, Chapter 12, 2008.
- Boogie-Style Software Verification
  - Tutorial Slides on Modular Verification and Differential Verification
  - Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. 2005. Boogie: a modular reusable verifier for object-oriented programs. In FMCO 2005.
  - Mike Barnett and K. Rustan M. Leino, Weakest-precondition of unstructured programs, in PASTE 2005.
- Software Model Checking
  - David Brumley. Software Model Checking Overview (Slides). 2012.
  - Ranjit Jhala and Rupak Majumdar. Software model checking. ACM Comput. Surv. 2009. [ACM Lib]
  - Elisabeth A. Strunk, M. Anthony Aiello, John C. Knight, Eds. A Survey of Tools for Model Checking and Model-Based Development. 2006.
  - E. Allen Emerson. The Beginning of Model Checking: A Personal Perspective. 25 Years of Model Checking, Orna Grumberg and Helmut Veith (Eds.). Lecture Notes In Computer Science, Vol. 5000. Springer-Verlag, Berlin, Heidelberg 27-45, 2008.
  - Edmund M. Clarke and Bernd-Holger Schlingloff. Model checking. Handbook of automated reasoning, Alan Robinson and Andrei Voronkov (Eds.). Elsevier Science Publishers B. V., Amsterdam, The Netherlands, The Netherlands 1635-1790, 2001.
- Symbolic Execution
  - Roberto Baldoni, Emilio Coppa, Daniele Cono D'Elia, Camil Demetrescu, Irene Finocchi. A Survey of Symbolic Execution Techniques.
- UMD Symbolic Execution Tutorial (based on KLEE)
  - Thomas BALL and Jakub DANIEL. Deconstructing Dynamic Symbolic Execution. 2014 Marktoberdorf Summer School on Dependable Software Systems Engineering. [Slides]
  - L. Cseppentő, Z. Micskei. Evaluating Symbolic Execution-based Test Tools. ICST 2015. [Project Web]
  - Cristian Cadar and Koushik Sen. Symbolic execution for software testing: three decades later. CACM 2013.
  - Cristian Cadar, Patrice Godefroid, Sarfraz Khurshid, Corina S. Păsăreanu, Koushik Sen, Nikolai Tillmann, and Willem Visser. Symbolic execution for software testing in practice: preliminary assessment. In ICSE 2011.
  - Corina S. Păsăreanu, Willem Visser. A survey of new trends in symbolic execution for software testing and analysis. International Journal on Software Tools for Technology Transfer. 2009.
- Giovanni Denaro. A Comparison Between Symbolic Execution-Based Verification and Model Checking. Tech Report. 2002.
  - Formalization of symbolic execution
- Dissertation:
  - Exploiting Trade-offs in Symbolic Execution for Identifying Security Bugs. Athanasios Avgerinos, CMU 2014.
  - Past
- Pointer Analysis
  - Yannis Smaragdakis and George Balatsouras. Pointer Analysis. Tutorial Notes. Foundations and Trends in Programming Languages. 2015.
- Information Flow Analysis
  - Anna Thoma. Secure Information Flow Using Compiler Techniques. UBC 517C Course Project Report. 2012.
  - Christian Hammer, Jens Krinke, and Gregor Snelting. Information Flow Control for Java Based on Path Conditions in Dependence Graphs. ISSSE 2006.
  - Christian Hammer and Gregor Snelting. Flow-Sensitive, Context-Sensitive, and Object-sensitive Information Flow Control Based on Program Dependence Graphs. International Journal of Information Security 2009.
- Program Slicing
  - K. Gallagher and D. Binkley. Program Slicing. Frontiers of Software Maintenance, 2008. fosm08-slicing.pdf slides
  - Frank Tip. A Survey of Program Slicing Techniques. 1995.
- Software Testing
  - Alessandro Orso and Gregg Rothermel. 2014. Software testing: a research travelogue (2000–2014). In FOSE 2014.
- Other testing surveys and testing dissertations

MSR Open Source Boogie (project web)
- Other papers on Boogie
- Open source projects using Boogie
  - Open Source .NET to Boogie Translator
  - Open Source C to Boogie Translator
- MSR Open Source SymDiff Project: Differential program verifier (project web)
- MSR Code Contract (project web, download)
MSR Pex Project
- PUT/C# Open Source Code

Operational semantics