Lectures
  • 1st LECTURE

    Introduction and Motivation. Evaluation.

  • 2nd LECTURE

    Hoare's CSP. Evolution of CSP. Syntax and intuitive semantics. Trace semantics. Failure semantics. The F2R Tool.

  • 3th LECTURE

    The Calculus of Communication Systems. Operators of CCS. Examples: a web service interaction scenario; a lossy communication medium. Syntax of CCS. Labeled transition systems and CCS labeled transition semantics. Derivation trees. Observational equivalence and approximations. Verification by checking equivalence between implementations and specification. Verification tools: the MWB (CCS fragment).

  • 4th LECTURE

    Motivation for bisimilarity. Strong Bisimilarity. Nondeterminism, internal and external choice. Examples.

  • 5th LECTURE

    Weak Bisimilarity. Behavioral equations with respect to strong and weak bisimilarity. Congruence of bisimilarities. Checking bisimilarity by manual calculation using equations.

  • 6th LECTURE

    Limitations of CCS. Motivation of pi-calculus. Examples of name mobility. Scope Extrusion. Representation of generic functional programs in the pi-calculus.

  • 7th LECTURE

    The pi-calculus. The operators of pi-calculus. Pi-calculus structural congruence. Pi-calculus labeled transition semantics. Strong Bisimilarity. Examples. Some basic behavioral identities (equations).

  • 8th LECTURE

    More pi-calculus examples. Specifications of concurrent systems via modal Logics. Henessy-Milner logic. Correspondence between Henessy-Milner logic and bisimilarity.

  • 9th LECTURE

    Modal logics. Review of Linear Temporal Logic (LTL), Computational Tree logic (CTL) and Hennessy-Milner Logic (HML). Spatial logics. Examples. The Spatial Logic Model Checker.

  • 10th LECTURE

    Models of secure systems. The spi-calculus and the applied pi-calculus. Examples. Process equivalences in the presence of cryptographic operators. Introduction to framed bisimilarity.

  • 11th LECTURE

    Representation of security properties in terms of behavioral equivalences: secrecy and autenticity properties. Examples. Definition of framed bisimilarity: knowledge frame and decryption closure.