CS6217 - Topics in Prog. Languages & Software Engineering (Semester-1, 2022/23)

Automata Theory, Logic and Games for the working PLSE researcher

In this module, we will study some foundational topics and techniques relevant for automated testing, verification and synthesis of computer systems. Automata theory and its connections to logic has traditionally played a foundational role in the development of decidability results in these contexts. As part of this module, we will cover a mixed bag of topics that will help students acquiant themselves with classical results and techniques used to establish these results. We also expect that knowledge of such results be useful in answering algorithmic questions in programming languages, software engineering and more generally in the analysis ans construction of computer systems. We will start with basic and slightly advanced topics in automata theory including DFAs, NFAs and automata on infinite words, together with their connections to logic. Such techniques have been widely applied in applications such as model checking, and also in proving some fundamental results in logic (such as decidability of various questions in fragments of second order logic). We will then look at related topics such as graph games, reactive synthesis, tree regular languages, rewriting logic. Finally, we will cover basics of probabilistic models of computation and some decidable fragments of first order logic.

The assessment for the module will be done by via quizzes, reviewing classical and/or recent papers, and a research project (in teams of at most 2 students). For more details on the specific topics, please refer to the Course Syllabus.

Prerequisites

Attendees must be fluent in Discrete Mathematics and must have taken a class in Theory of Computation module. Familiarity with logic (propositional logic) is preferred.

Module Logistics

  • Grading Policy

  • Instructor: Umang Mathur

  • Lectures: Thursdays, 10:00-12:00pm. First lecture on August 11, 2022.

  • Location: COM1, VCRM, COM1-02-13 (next to the Student Lounge on COM1 Level 2)

  • Office hours: arranged on demand by appointment

Lecture Notes (Weeks 1-4)

The remaining lecture notes will be posted gradually as we progress through the course.

Grading Policy

To be decided…

Textbooks and Resources

To be updated…