Description
- Concurrency and Communication
- Principles of Concurrent Communicating Systems: mechanisms, languagens, analysis.
- Modeling concurrent systems based on communication and shared actions: the CSP and CCS models.
- Observational equivalence of CCS processes. Liveness and Safety Properties. Behavioral Algebras.
- Verification by equivalence checking and using modal logics. Model-checking algorithms for both approaches.
- Modal logics for concurrent systems: temporal logic, hennessy-milner logic, spatial logics.
- Models of several concurrent and distributed algorithms, inspired by scenarios of distributed computation, workflow management, mobile computing, embedded systems, etc.
- Verification tools (F2R, MWB, SLMC).
- Mobility and Security
- Modeling reconfigurable systems based on name passing: the Pi and Applied Pi-calculus models.
- Bisimilarity and observational equivalence of processes in Applied Pi.
- Fundamental principles of secure communication and computation and concrete applications. Abstraction levels in models of security properties. The Dolev-Yao model and the perfect cryptography assumption.
- Specification and analysis of security properties: confidentiality and autenticity.
- Case studies. Tools for security protocol analysys (Cryptic, Proverif).
Resources
