Verification of Embedded Systems

Module nameVerification of Embedded Systems
Type of moduleSelectable mandatory module
Learning results,
competencies, qualification goals		The student is able to:
  • define data flow analyses for imperative programmes independently,
  • explain the fundamentals of abstract interpretation (partial orders, Galois relations, abstract transformers),
  • apply static programme analyses to programmes with pointers,
  • use static programme analyses to gain an estimation of the runtimes of embedded systems.

Learning results with regard to the objectives of the course of study:
  • Gaining deeper insight into the mathematical and natural science areas
  • Gaining a deeper knowledge about the specific electrical fundamentals
  • Acquiring enhanced and applied subject-specific basics
  • Identifying and classifying complex electro-technical and interdisciplinary tasks
  • Being confident in the ability to apply and evaluate analytical methods
  • Being able to create and evaluate solving methods independently
  • Familiarising oneself with new areas of knowledge, running searches and assessing the results
  • Gaining important and profound experience in the area of practical technical skills and engineering activities
  • Working and researching in national and international contexts
Types of courses4 SWS (semester periods per week):       3 SWS lecture
                                                                 1 SWS exercise
Course contents
  • Data Flow Analysis
  • Abstract interpretation
  • Shape analysis of pointer manipulating programs
  • Worst-case execution time analysis
Teaching and learning methods
(forms of teaching and learning)		Lecture, presentation, learning by teaching, self-regulated learning, problem-based learning
Frequency of the module offeringWinter term
Language English
Requirements for the
participation in the module		Prerequisites according to examination regulations
Student  workload180 h:   60 h attendance studies
             120 h personal studies
Academic performancesNone
Precondition for the
admission to the
examination performance		None
Examination performanceWritten examination (90 min.)
Number of credits
of the module		6 credits

In charge of the moduleProf. Dr. Kreiker
Teacher of the moduleProf. Dr. Kreiker and co-workers
Forms of mediaProjector, black board, piece of paper
Literature references
  • Slides of this lecture
  • Nielson, Nielson, Hankin: Principles of Programming Analysis, Springer 2004.
  • Additional current research articles will be announced in the lecture.

                                                 Back to Modules page