Project

Presentation Schedule

Group 1

1. Complexity Analysis
2. MIRAI
3. GENTREE
4. EYE TRACKING
5. PMD
6. NNV

Group 2

1. PMD: WP
2. FLOW: MM
3. ANGR: LL
4. MYPY: PM
5. INFER: JS
6. PYRE/PYSA: ES

Overview

• Each student will complete an individual project, which helps explore more deeply a topic covered in the course (or a related topic which we didn't cover).

• There are two type of projects: understand existing and creating new tools. Important: graduate students MUST choose the second type.

• Learning an existing program testing, verification, or analysis tool. This type of project typically involves

  1. learn about the problem the tool is trying to solve
  2. learn how to use the tool
  3. demonstrate how the tool works on concrete and challenging examples. Also include example where the tool fails to work to understand what it can and cannot do
  4. evaluate the tool on some real-world, medium/large software
  5. Tools examples are given below. You can provide additional suggestions to work on some tools you're interested in (but you must discuss with me first).
  6. IMPORTANT: you must be able to get a tool installed/run on your machine BEFORE you propose to work on it. This is to avoid the problem where you select some tool and at the end cannot install/run it and give up.

• Creating (i.e., implementing) a new TVA technique or extending an existing one. You will work on developing some TVA tool and evaluate it thoroughly. This work is typically more challenging than the first one. If you're a graduate student, you must select this option. For undergraduate student, you are also welcome to do this (but if you select this, I expect you to follow it through). This type of project involves

  1. select a TVA problem you want to solve and do some survey on existing approaches on solving it
  2. create new or extend an existing technique to solve the problems.
  3. implement the technique as tool (no restriction on language or machine, you can work on your own computer and use whatever languages you want)
  4. demonstrate how the tool works on concrete and challenging examples. Also include example where the tool fails to work to understand what it can and cannot do
  5. Potential topics are listed below. You can choose your own but you must talk to me first if you do this.

• Formats: See this example for what to write (for both proposals and report): https://cse.unl.edu/~goddard/WritingResources/Templates/Generic-Technical-Paper-Skeleton.html

Proposal

• submit a project proposal (1-2 page) that explains what you want to do and what you expect to learn from the project
• Here is a proposal example, and the TeX source code (running make will build the pdf)
• You can use LaTex or Word to write your proposal, but you must turn in a PDF version file named proposal-last-firstname.pdf.

Report

• Submit a project report (4-5 pages for double-column report).
• You will write a formal report on what you did (e.g., using LaTeX and including all the sections such as Introduction, Body, Related Work, Conclusion).
• You can use Word or Latex, but you must turn in a PDF version of your paper (report-last-firstname.pdf). Here's an outline of what usually should be in the final report

Presentation

You will give a 10 min presentation of your project at the end of the semester. The presentation will include running demo's on how your program/tool works on some interesting examples. You can use the report outline to structure your presentation.

---

Potential Tools/Topics

Tools

crossed out: the tool has been selected by someone

1. ANGR: Static and dynamic symbolic (concolic) analysis for binaries
2. Mypy: static type checker for Python
3. PMD: Static Source Code analyzer for Java and other languages
4. Soot: Framework for analyzing and transforming Java and Android apps
5. CBMC: bounded model checking tool for C
6. Facebook Pyre and Pysa: type checking and static analysis tool for Python
7. Flow: A static type checker for JavaScript
8. Z3: SMT Solver (used by many static analysis tools)
9. JPF: model checking tool for Java
10. Facebook Infer: bug checking tool for C and Java
11. Sketch: Program synthesis tool
12. Randoop and EvoSuite: Search-based test generation tools (if you pick this, you need to do both tools)
13. Frama-C: source-code analysis for C programs
14. Ultimate: verification tool for C programs
15. Daikon: Dynamic Invariant Generation tool for Java programs
16. DIG: Dynamic + Symbolic Execution approach for inferring numerical program invariants
17. SPIN: Verifying multi-threaded software
18. Symbolic PathFinder (SPF): symbolic execution tool for Java
19. CPAChecker: Configurable Program Analysis tool for C programs
20. Eran: verification tool for Deep Neural Network
21. NNV: Matlab toolbox to verify Deep Neural Network (Note: you cannot select this if you are currently enrolling in the Deep Learning Assurance class (which uses this tool extensively))

Topics

1. Validating Array Invariants: use existing checking tools, , e.g., Symbolic Execution, to validate assertions involving array/list variables (potential tools: SPF, CPAChecker)
2. Validating Complex Data Invariants: use existing tools, e.g., Symbolic Execution, to validate assertions capturing required properties of data structures such as trees, heaps
3. Inferring Algebraic Specifications: synthesize specifications describing relations among program methods, e.g., pop(pus(Stack_A)) == Stack_A
4. Infer high-coverage input interactions: discover interactions over configuration options leading to high code coverage
5. Use Genetic Algorithm to find data structure inputs leading to high program complexity
6. Use Genetic Algorithm to repair buggy Python programs (benchmark: Quixbugs benchmark)
7. Extend DIG (Dynamic Invariant Generation) to work with additional abstract domain (zonotopes, bags, triangle, star set, etc)
8. Dynamically infer invariants for Deep Neural Networks
9. Create Fuzzing techniques (AFL, GA, etc) to test Neural Networks
10. Discovering program complexity from runtime information
11. Analyzing Interactions in Highly Configurable Systems
12. Extending MIRAI (verification tool for RUST) with Octagonal Abstract Domain

Links

• Main page