This is a list of areas for final projects. It is acceptable for multiple teams to pick the same area; however, in that case we would need to  only want each team to pick one of these projects.

• Model checking:
  • The SPIN model checker. Holtzmann, 1997.
  • The SPIN system.
• Abstract interpretation:
  • The Apron library for numerical abstract domains.
• Probabilistic verification:
  • Stochastic model checking. Kwiatkowska, Normal, Parker, 2007.
  • The PRISM system.
• Syntax-guided synthesis:
  • Syntax-guided synthesis. Alur et al, 2013.
  • The SKETCH system.
  • The Sygus competition page.
• Programming by example.
  • Synthesizing data structure transformations from input-output examples. Feser, Chaudhuri, Dillig, 2015.
  • The Lambda2 program synthesizer.
• Liquid types:
  • Liquid types. Rondon, Kawaguchi, and Jhala.
  • The Liquid Haskell system.
• Separation logic:
  • A primer on separation logic. Peter O’Hearn.
  • Viper: A Verification Infrastructure for Permission-Based Reasoning. Müller, Schwerhoff, and Summers, 2016.
  • The Viper proof system.
• Statistical program synthesis:
  • Neural sketch learning for conditional program generation. Murali, Qi, Chaudhuri and Jermaine, 2018.
  • The Bayou synthesizer.