This course has been re-designed (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,
conflict-driven 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 finite-state automata on finite words, subset
construction, regular expressions, pumping lemma
- (Non)-Deterministic finite-state automata on infinite words:
omega-regular languages, non-deterministic 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.
|