Back close
Admissions

Course Detail

Course Name Formal Methods
Course Code 21SN648
Program M. Tech. in Cyber Security Systems & Networks
Credits 3

Overview

Background: Computability and Complexity, Decidability, Semi-decidability, Undecidability, Halting problem, Rice’s theorem, Overview of complexity classes: P, NP, NP-completeness. Propositional and First-Order Logic: Syntax, Semantics, Proof methods , Program Verification: Floyd-Hoare logic, Weakest Pre-conditions; Partial Correctness and Termination Structural induction and Fixed-point induction for recursive procedures

Z specification language: Fundamentals and abstract data type specifications. Data refinement in Z abstract data types: Forward and backward simulation, Concurrent Programs and Correctness Properties: Owick-Gries, Assume-Guarantee, Reactive Systems: Transformational vs Reactive systems, Temporal Logic: Linear (LTL) and Branching Time (CTL), Temporal specification of reactive systems: Safety, Liveness, Fairness, Buchi automata, LTL-to-Buchi automata, Properties: containment, emptiness, Model Checking: LTL and CTL model-checking. Analysis of model-checking algorithms Symbolic model checking; overview of state-space reduction methods, Case study and practical verification of properties, Process Algebra: CCS and Pi-calculus, Reductions and labelled transitions, Harmony lemma, Bisimulations

 

TEXT BOOKS / REFERENCES:

  1. E.M. Clarke, O. Grumberg, and D. Peled “Model Checking”, 2nd Edition, MIT Press, 2018.
  2. DavideSangiorgi and David Walker, “Pi-calculus: The Theory of Mobile Processes”, Cambridge University Press,2003
  3. SanjeevArora and Boaz Barak, “Computational Complexity – A Modern Approach”, Cambridge University Press, 2017
  4. Michael Huth and Mark Ryan, “Logic in Computer Science”. 2nd Edition, Cambridge University Press, 2004.
  5. J. Woodcock & J. Davies “Using Z: Specification, Refinement and Proof”, Prentice Hall, 1994.

Course Objectives

  • CO1: Get an understanding of the background in Formal Methods and learn the different types of classes.
  • CO2: See the different type of proof methods and apply them to Security applications
  • CO3: Learn about the different type of Correctness properties and know when to use them
  • CO4: Have a good understanding on analysis of models

DISCLAIMER: The appearance of external links on this web site does not constitute endorsement by the School of Biotechnology/Amrita Vishwa Vidyapeetham or the information, products or services contained therein. For other than authorized activities, the Amrita Vishwa Vidyapeetham does not exercise any editorial control over the information you may find at these locations. These links are provided consistent with the stated purpose of this web site.

Admissions Apply Now