Modelling and Verification


Recommended prerequisite for participation in the module

The module builds on knowledge gained in the course: Syntax and Semantics

Content, progress and pedagogy of the module

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


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.


  • 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


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

Type of instruction

The teaching is organized in accordance with the general teaching methods for the education, cf. section 17.

Extent and expected workload

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



Name of examModelling and Verification
Type of exam
Written or oral exam
Assessment7-point grading scale
Type of gradingInternal examination
Criteria of assessmentThe criteria of assessment are stated in the Examination Policies and Procedures

Additional information

Contact: Study Board for Computer Science via or 9940 8854

Facts about the module

Danish titleModellering og verifikation
Module codeDSNDATB612
Module typeCourse
Duration1 semester
Language of instructionDanish and English
Empty-place SchemeYes
Location of the lectureCampus Aalborg
Responsible for the module


Education ownerBachelor of Science (BSc) in Computer Science
Study BoardStudy Board of Computer Science
DepartmentDepartment of Computer Science
FacultyThe Technical Faculty of IT and Design