Programming Languages, Formal Methods, Software Engineering (PLFMSE)

Qualification Exam Requirements

Students who enrolled for their PhD *before* Fall 2022 can choose to follow these new rules or follow the old rules from https://plfmse.cs.illinois.edu/before2022 . Students who enrolled from Fall 2022 or after have to follow these new rules as described below.

The qualifying exam for PL/FM/SE consists of an oral exam to be scheduled for exactly 2 hours (120 minutes), where students will be asked to (1) present one paper assigned to them based on their interests and (2) answer questions on various topics related to the subareas of their choosing. The paper will be assigned two to three weeks before the exam date, based on the research interests listed in the Qual Statement form.

The process is as follows. Our area has three subareas: Programming Languages (PL), Formal Methods (FM), and Software Engineering (SE). Each student is required to pick a major subarea and two minor subareas. The two minor subareas can also be from the Architecture/Compiler/Parallel or Systems/Networking areas. Students must indicate the choice of subareas in their Qual Statement. For the major (respectively, minor) subarea, the students have to choose 4 (respectively, 3) of the N topics listed for the subarea.

Each subarea has a reading list (see below). Students are expected to field questions that are in these lists as well as any basic computer science material we would expect of a student in computer science.

Programming Languages

Of the following 5 topics, choose 4 (if major subarea) or 3 (if minor subarea):

1. Background reading on Hoare Logic by Mike Gordon; Chapters 1 and 2
   (Courses: CS477; CS476; CS522)
2. Type Theory (choose one):
   1. A Theory of Type Polymorphism in Programming Robin Milner
      Journal of Computer and System Sciences 17(3), 1978
      (Courses: CS422, CS522)
   2. An Introduction to Generalized Type Systems Henk (Hendrik) Pieter Barendregt
      Journal of Functional Programming 1(2), 1991
3. Object-Oriented Programming (choose one):
   1. Dimensions of Object-Based Language Design Peter Wegner
      ACM SIGPLAN Notices 22(12), 1987
      (Courses: OO concepts in CS422, CS522)
   2. Concurrent Object-Oriented Programming Gul Agha
      Communications of the ACM 33(9), 1990
      (Courses: CS524, concurrent OO concepts in CS422)
4. Syntax-Guided Synthesis Rajeev Alur et al.
   NATO Science for Peace and Security Series - D: Information and Communication Security 40, 2015
5. Probabilistic Programming (choose one):
   1. Static Analysis for Probabilistic Programs: Inferring Whole Program Properties from Finitely Many Paths Sriram Sankaranarayanan, Aleksandar Chakarov, Sumit Gulwani
      PLDI 2013
      (Course: CS521Misailovic)
   2. Commutative Semantics for Probabilistic Programming Sam Staton
      ESOP 2017
      (Course: CS521Misailovic)

   Formal Methods

   Background material that you should know: propositional logic and predicate logic, basic automata theory and theory of computation, basic theory of algorithms, basic discrete mathematics. (see old website for some references)

   Of the following 7 topics, choose 4 (if major subarea) or 3 (if minor subarea):

   1. Background reading on Hoare Logic by Mike Gordon; Chapters 1 and 2
      (Courses: CS477; CS476; CS522)
   2.  Software Model Checking Ranjit Jhala, Rupak Majumdar
      ACM Computing Surveys 41(4), 2009
      (Courses: CS477)
   3. Abstract Interpretation Frameworks Patrick Cousot, Radhia Cousot
      Journal of Logic and Computation 2(4), 1992
      (Courses: CS 477, CS 526)
   4. Lecture Notes on Logic in Computer Science
       P. Madhusudan, Mahesh Viswanathan
      (Courses: CS474, CS476)
   5. Theorem Proving (choose one):
      1. A Metalanguage for Interactive Proof in LCF M. J. C. Gordon, R. Milner, L. Morris, M. C. Newey, C. P. Wadsworth, POPL 1978
      2. The Foundation of a Generic Theorem Prover Lawrence C. Paulson Journal of Automated Reasoning 5(3), 1989
   6. Formal Certification of a Compiler Back-end or: Programming a Compiler with a Proof Assistant Xavier Leroy, POPL 2006
   7. Sound, Complete and Scalable Path-Sensitive Analysis Isil Dillig, Thomas Dillig, Alex Aiken, PLDI 2008

   Software Engineering

   Of the following 5 topics, choose 4 (if major subarea) or 3 (if minor subarea):

   1. Test-Input Generation (choose one):
      1. CUTE: A Concolic Unit Testing Engine for C  Koushik Sen, Darko Marinov, Gul Agha, ESEC/FSE 2005
      2. Whole Test Suite Generation  Gordon Fraser, Andrea Arcuri, TSE 2012
   2. Test Oracles (choose one):
      1. Dynamically Discovering Likely Program Invariants to Support Program Evolution Michael D. Ernst, Jake Cockrell, William G. Griswold, David Notkin
         IEEE Transactions of Software Engineering 27(2), 2001
      2. The Oracle Problem in Software Testing Earl T. Barr, Mark Harman, Phil McMinn, Muzammil Shahbaz, Shin Yoo
         IEEE Transactions of Software Engineering 41(5), 2015
   3. Machine Learning for Code (choose one):
      1. On the Naturalness of Software  Abram Hindle, Earl Barr, Mark Gabel, Zhendong Su, Prem Devanbu, ICSE 2012
      2. CodeBERT: A Pre-Trained Model for Programming and Natural Languages Zhangyin Feng, Daya Guo, Duyu Tang, Nan Duan, Xiaocheng Feng, Ming Gong, Linjun Shou, Bing Qin, Ting Liu, Daxin Jiang, Ming Zhou
         EMNLP 2020
   4. Debugging (choose one):
      1. Staged Program Repair with Condition Synthesis  Fan Long, Martin C. Rinard, ESEC/FSE 2015
      2. A Survey on Software Fault Localization  W. Eric Wong, Ruizhi Gao, Yihao Li, Rui Abreu, Franz Wotawa
         IEEE Transactions of Software Engineering 42(8), 2016
   5. Regression Testing Minimization, Selection and Prioritization: A Survey Shin Yoo, Mark Harman
      Software Testing, Verification & Reliability Journal 22(2), 2012 [Sections 1-5 are required]