This course is divided in two modules, namely automated reasoning and program verification. Automated reasoning will include advance design of SAT solvers, theory combination, decision procedures for various first-order theories, proof generation, maxsat, model counting, quantifier elimination, interpolation, abduction, etc. Program verification will include program modelling, concolic testing, abstract interpretation, symbolic model checking, bounded model checking, abstract refinement based model checking, concurrency verification, and termination proving. The course work will include theoretical as well as practical exercises.