This course has been redesigned (from its earlier avatar) to be a
foundational breadth course primarily for students who wish to
pursue advanced studies in formal methods and/or pursue research
and development projects in this exciting area. The course will
also be useful for those desirous of pursuing studies/research in
programming languages and program analysis. It will cover a wide
breadth of topics in logic, automata, formal proofs, decision
procedures and their applications to some formal verification
problems. We will review and then build on topics prescribed in
the GATE CS syllabus for theory of computation. The course
presumes that students have gone/are concurrently going through an
undergraduate course on theory of computation, discrete structures
and algorithms.
The list of topics to be covered in the course includes:
 Propositional logic: syntax and semantics, truth table,
satisfiability proof systems, equivalences, normal forms, Tseitin
encoding
 FOL (First order logic): syntax and semantics, SAT problem
in FOL, proof systems, FOL Theories
 Simple programming language, small and big step semantics,
strongest postcondition, weakest preconditon, Hoare logic,
invariants, tools for invariant checking
 Satisfiability (SAT) solvers for propositional logic,
conflictdriven clause learning (CDCL) and optimizations,
examples of encoding problems into SAT problems,
satisfiability modulo theory (SMT) solvers
 Linear temporal logic (LTL) and Computation tree
logic(CTL): syntax and semantics, normal forms, satisfiability
problems
 (Non)Deterministic finitestate automata on finite words, subset
construction, regular expressions, pumping lemma
 (Non)Deterministic finitestate automata on infinite words:
omegaregular languages, nondeterministic Buchi automata and LTL,
emptiness checking.
 Basic notions of computability, Turing machines, undecidability
IMPORTANT: Students are required to put in 4 to 6 hours of reading
per week beyond the contact hours in class.
