CS 6340
Software Analysis and Test
Fall 2022
Announcements:

Instructor:
Qirun Zhang,
Office: 2324 Klaus
Office Hours: Tue/Thu 4:45 - 5:30 PM
Email: qrzhang@gatech.edu

Teaching Assistant:
Yuanbo Li,
Office: By appointment
Office Hours: Monday 10 AM - 11 AM
Email: yuanboli@gatech.edu

Lectures:
Time: Tue/Thu 3:30 PM - 4:45 PM
Location: Howey Physics L5*
Zoom link: Click to join.

Course Summary:
CS 6340 is a graduate-level course on software analysis and testing. We will cover topics such as static program analysis, random testing, dataflow analysis, type systems, test case generation, symbolic execution, and more. We will also study selected papers from PL conferences such as POPL and PLDI.

References:

Assignments:
  • Paper Review
    • Paper review LaTeX template.
    • Deadline: by 10:00 pm EST the night before the class.

  • Project Proposal
    • Four-Paragraph guideline for your proposal.
    • Deadline: 10/1 by 10:00 pm EST.

  • Project Report
    • Conference-paper-style report.
    • Deadline: 11/26 by 10:00 pm EST.

Grading:
Grading breakdown:
  • Paper Review: 20%
  • Presentation: 20%
  • Project: 60%

Late assignment submission policy:
  • Within 24 hours after the assignment is due: 50% point deduction;
  • More than 24 hours late: 100% point deduction.

Schedule:

Date Topic Paper Presenter and Optional Reading
8/23 Introduction
8/25 Fundamentals
8/30 Fundamentals
  • Type analysis
  • Qirun
  • Readings:
    • [MS18] Chapter 3.
9/1 Range analysis
  • [PLDI'20] Towards a verified range analysis for JavaScript JITs
9/6 Fundamentals
  • Flow-sensitive analyses
  • Qirun
  • Readings:
    • [MS18] Chapters 4 and 5.
9/8 Graph reachability
  • [POPL'95] Precise Interprocedural Dataflow Analysis via Graph Reachability
9/13 Value-flow analysis
  • SVF: interprocedural static value-flow analysis in LLVM
  • Yuanbo
9/15 Value-flow analysis application
  • [TSE'14] Detecting Memory Leaks Statically with Full-Sparse Value-Flow Analysis
9/20 Symbolic Execution
  • Notes
  • Qirun
9/22 Translation Validation
  • [PLDI'21] Alive2: Bounded Translation Validation for LLVM
9/27 Floating-point safety
    [PLDI'21] High Performance Correctly Rounded Math Libraries for 32-bit Floating Point Representations
9/29 Taint analysis
  • Notes
  • Qirun
10/4 Project Proposal
  • All
10/6 Compiler testing
  • [PLDI'17] Skeletal Program Enumeration for Rigorous Compiler Testing
10/11 Fundamentals
  • Path sensitivity and relational analysis
  • Qirun
  • Readings:
    • [MS18] Chapter 7.
10/13 Path-sensitive analysis
  • [PLDI'21] Path-Sensitive Sparse Analysis without Path Conditions
10/18 No class
10/20 SMT solvers
  • [PLDI'21] Boosting SMT Solver Performance on Mixed-Bitwise-Arithmetic Expressions
10/25 Fundamentals
  • Interprocedural and context sensitive analysis
  • Qirun
  • Readings:
    • [MS18] Chapter 8.
10/27 Bug finding
  • [PLDI'22] Finding Typing Compiler Bugs
11/1 Fundamentals
  • Pointer analysis
  • Qirun
  • Readings:
    • [MS18] Chapter 10.
11/3 Program efficiency
  • [PLDI'22] Choosing mathematical function implementations for speed and accuracy
11/8 Random Testing
  • Notes
  • Qirun
11/10 WebAssembly
  • [PLDI'22] Finding the Dwarf: Recovering Pecise Types from WebAssembly Binaries
11/15 Delta debugging
  • Notes
  • Qirun
11/17 Test-case reduction
  • [PLDI'21] Test-Case Reduction and Deduplication Almost for Free with Transformation-Based Compiler Testing
11/22 Bounded model checking
  • [CAV'14] Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization
11/24 No class
11/29 Final Presentation
  • All
12/1 Final Presentation
  • All

Misc:
If you have any concern, please send an email to the instructor. This link could help to send anonymous messages.

* In-person attendance is not enforced. We will record each lecture. The recorded video will be shared on Zoom.