COURSE SUMMARY
Course Title: 
Formal Methods
Course Code: 
18SN703
Year Taught: 
2018
Degree: 
Postgraduate (PG)
School: 
School of Engineering
Center: 
Cyber Security
Campus: 
Amritapuri

"Formal Methods" is an elective course offered in M. Tech. in Cyber Security Systems & Networks program at School of Engineering, Amrita Vishwa Vidyapeetham, Amritapuri.

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

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