Selected Topics in Modelling and Verification


Content, progress and pedagogy of the module

Learning objectives


The student should gain knowledge of recent research in advanced mathematical models for formal description and verification of programs, software systems and programming languages. These can, e.g. be

  • Binary Decision Diagrams (BDD)
  • SAT algorithms
  • predicate logic
  • Petri nets, temporal logic
  • mobile process calculations.


  • be able to explain precisely and using the terminology and notation of the subject important important theories for description and analysis of software systems;
  • be able to use specification and verification methods based on formal models;
  • be able to make use of the necessary writing skills in this context


  • be able to use formal models and associated verification tools for description, analysis and verification of software systems

Type of instruction

The type of instruction is organised in accordance with the general instruction methods of the programme, cf. § 17.

Extent and expected workload

It is expected that the student uses 30 hours per ECTS, which for this activity means 150 hours



Name of examSelected Topics in Modelling 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: The Study board for Computer Science at or 9940 8854

Facts about the module

Danish titleUdvalgte emner inden for modellering og verifikation
Module codeDSNCSITK226
Module typeCourse
Duration1 semester
Language of instructionEnglish
Empty-place SchemeYes
Location of the lectureCampus Aalborg
Responsible for the module


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