Recommended prerequisite for participation in the module

Content, progress and pedagogy of the module

Disclaimer.
This is an English translation of the module. In case of discrepancy between the translation and the Danish version, the Danish version of the module is valid.

Learning objectives

Knowledge

The student must acquire knowledge of advanced mathematical models for formal description and verification of programs, software systems and programming languages ​​with a focus on parallel and communicating systems. In particular, the student must acquire knowledge of:

• transition systems
• process algebra, e.g. CCS
• bisimulation
• Hennessy-Milner logic with recursion
• Tarski's theorem on fixed points
• models and reasoning methods for real-time systems, such as Timed CCS and time machines
• verification techniques for real-time models
• possibly other topics from model verification such as partial order reduction or probabilistic models and reasoning techniques

The course module can also include other formal models.

Skills

• be able to explain accurately and using the subject's terminology and notation for important theories for description and analysis of reactive systems
• be able to use verification tools based on formal models
• be able to make use of the necessary written skills in these contexts

Competences

• be able to use formal models and related verification tools to verify software systems

Type of instruction

Extent and expected workload

The student is expected to spend 27.5 hours per ECTS, which for this activity means 137.5 hours.

Exam

Exams

Additional information