Course

Syllabus

Formal Methods – Propositional and Predicate logic, and theorem-proving, Fixed-points and their role in program analysis and model-checking, Verification of sequential programs using weakest preconditions and inductive methods, and verification of concurrent and reactive programs/systems using model-checking and propositional temporal logic (CTL and LTL), Application of static and dynamic program analysis and model-checking for detecting common security vulnerabilities in programs and communication protocols, Information flow and taint analysis for security of web applications, pi-calculus for formal modelling of mobile systems and their security. SPIN, PVS, TAMARIN, Frama-C, and Isabelle tools, Case study on applying formal methods for system call specification and verification.

Prerequisite

Logic and Discrete Mathematics

Course Outcome

CO-PO Mapping

1. Edmund M. Clarke, Orna Grumberg and Doron Peled, Model Checking, MIT Press, 1999.
2. Lloyd, J.W., Logic and Learning: Knowledge Representation, Computation and Learning in Higher-order Logic, Springer Berlin Heidelberg, 2003.
3. M. Ruth and M. Ryan, Logic in Computer Science – Modelling and Reasoning about Systems, Cambridge University Press, 2004.
4. G. Bella, Formal Correctness of Security Protocols, Springer, 2009.
5. Datta A, Jha S, Li N, Melski D, and Reps T, Analysis Techniques for Information Security, Synthesis Lectures on Information Security, Privacy, and Trust, 2010.