CSE6049
CSE6049 Program Analysis
News
- HW3 is out! (due date: 6/14 (Fri) 24:00)
- HW2 is out! (due date: 5/31 (Fri) 24:00)
- HW1 is out! (due date: 4/19 (Fri) 24:00)
Basic Information
- Instructor: Woosuk Lee
- Office Location: Rm#403, Eng. Bldg 3
- Telephone: 031-400-1031
- Email: woosuk at hanyang.ac.kr
- Office Hours: Monday 10:00 - 12:00
- Time & Location
- Friday 09:00 - 12:00 @ Rm#416, Eng. Bldg 4
References
- The course textbook: Static Program Analysis by Moeller and Schwartzbach
- Materials from related courses: CS6340: Software Analysis and Testing at Georgia Tech
- Program Analysis: Theories and Practices at Seoul Nat’l Univ.
Student presentation
Slides
- Introduction to Program Analysis: pdf
- Introduction to Software Testing: pdf
- Random Testing: pdf
- Automated Test Generation: pdf
- Dataflow Analysis: pdf
- Pointer Analysis: pdf
- Datalog Analysis: pdf
- Type Systems: pdf
- Abstract Interpretation (part 1): pdf
- Abstract Interpretation (part 2): pdf
- Delta Debugging: pdf
- Program synthesis: pdf
Grading
- Homework: 70%
- Student presentation: 20%
- Attendance: 10%
Reating Material
Reading material related to the lesson
- Introduction to Software Analysis
- What is static program analysis? talk by Matthew Might.
- Explains why program analysis is undecidable and develops a static analysis to play with in Racket.
- Lessons from Building Static Analysis Tools at Google
- Describes experiences developing and deploying program analysis tools at Google.
- What Developers Want and Need from Program Analysis: An Empirical Study
- One of the best empirical studies about program analysis.
- The Coming Software Apocalypse
- Overview of the state of software reliability problems and solutions to overcome them.
- From Start-ups to Scale-ups: Opportunities and Open Problems for Static and Dynamic Program Analysis
- Describes experiences developing and deploying program analysis tools at Facebook.
- What is static program analysis? talk by Matthew Might.
- Introduction to Software Testing
- Pex and Moles
- Unit test generation tools in Visual Studio for .NET programs.
- Hints on Test Data Selection: Help for the Practicing Programmer
- Original paper that introduced the idea of mutation testing.
- A Theory of Predicate-Complete Test Coverage and Generation slides
- Introduces a new code coverage metric based on predicates.
- Pex and Moles
- Random Testing
- A Randomized Scheduler with Probabilistic Guarantees of Finding Bugs, ASPLOS 2010
- Describes fuzz testing in Microsoft’s Cuzz tool to find concurrency bugs.
- QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs, ICFP 2000 video
- Describes fuzz testing in the QuickCheck tool to test properties of Haskell programs.
- Evaluating Fuzz Testing, CCS 2018 blog post
- Describes flaws in past evaluations of fuzz testing and gives guidelines going forward.
- A Randomized Scheduler with Probabilistic Guarantees of Finding Bugs, ASPLOS 2010
- Automated Test Generation
- Korat: Automated Testing Based on Java Predicates, ISSTA 2002
- Paper that introduced Korat.
- Feedback-Directed Random Test Generation, ICSE 2007 Randoop webpage
- Paper that introduced Randoop.
- NEZHA: Efficient Domain-Independent Differential Testing, IEEE S & P 2017 video
- A general differential testing approach to find bugs in binaries.
- Finding and Understanding Bugs in C Compilers, PLDI 2011 CSmith
- Adapts differential testing to find bugs in various C compilers.
- DeepXplore: Automated Whitebox Testing of Deep Learning Systems, SOSP 2017 video
- Adapts differential testing to find bugs in deep neural networks.
- Korat: Automated Testing Based on Java Predicates, ISSTA 2002
- Pointer Analysis
- Pointer Analysis, Foundations and Trends in Programming Languages, 2015
- Recent survey of pointer analysis.
- Pointer Analysis, Foundations and Trends in Programming Languages, 2015
- Inter-Procedural Analysis
- Undecidability of Context-Sensitive Data-Dependence Analysis, ACM TOPLAS, 2000
- Proof of undecidability of tracking calls/returns and reads/writes simultaneously.
- Undecidability of Context-Sensitive Data-Dependence Analysis, ACM TOPLAS, 2000
- Abstract Interpretation
- Abstract Interpretation Based Formal Methods and Future Challenge
- A good overview of Abstract Interpretation framework
- Comparing the Galois Connection and Widening/Narrowing Approaches to Abstract Interpretation
- An interesting theorem about the power of widening and narrowing
- Design and Implementation of Sparse Global Analyses for C-like Languages
- Describes how to accelerate existing static analyses without precision loss
- A Static Analyzer for Large Safety-Critical Software
- Describes how to apply abstract interpretation into formal verification of AirBus software
- Abstract Interpretation Based Formal Methods and Future Challenge
- Type Systems
- Type Systems, CRC Handbook, 2004
- Delta Debugging
- Effective Program Debloating via Reinforcement Learning, CCS 2018, webpage
- Describes how to accelerate program reduction using a machine learning-based approach
- Test-Case Reduction for C Compiler Bugs, PLDI 2012, webpage
- Program reducer specialized for isolating C compiler bugs
- Effective Program Debloating via Reinforcement Learning, CCS 2018, webpage
- Program Synthesis
- Syntax-guided Program Synthesis, FMCAD 2013, webpage
- The standard formulation of program synthesis problems
- Accelerating search-based program synthesis using learned probabilistic models, PLDI 2018, code
- Describes how to accelerate program synthesis using probabilistic models for code
- Others
- Syntax-guided Program Synthesis, FMCAD 2013, webpage