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

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

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