Back close

Course Detail

Course Name Formal Methods
Course Code 18SN703
Program M. Tech. in Cyber Security Systems & Networks
Credits Amritapuri
Year Taught 2018


Course Syllabus

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

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


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

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