Description: Over the last five to ten years the use of model checking and static
  analysis techniques to verify and validate "real-life" software has
  seen explosive growth.

  The aim of this course is to provide students with a thorough
  understanding of fundamental and foundational issues in both model
  checking and static analysis that will enable the students to use,
  adapt, and extend these techniques for their own work.

  The course will cover such topics as syntax, semantics, and model
  checking for temporal logics, e.g., LTL and CTL; the mu-calculus;
  software model checking (predicate abstraction, CEGAR, etc.);
  abstract interpretation (including the necessary background on
  domain theory and denotational semantics); and Flow Logic. The
  specific topics will be determined in cooperation with the students.

  Students are expected to have working knowledge of temporal logics
  and model checking, e.g., through the SV course, a good
  understanding of (operational) semantics, e.g., through the SS and
  SPO courses, as well as basic grasp of discrete mathematics for
  computer science, including pre- and partial-orders.

  Lectures and exercises.

Organizer: Prof. Kim G. Larsen <> and Assoc. Prof. Rene Rydhof Hansen <>

Lecturers: Prof. Kim G. Larsen <> and Assoc. Prof. Rene Rydhof Hansen <>

ECTS: 2.5

Time: 6-8 course sessions in November-December 2014

Place: Dept. Computer Science, Aalborg University

Zip code: 9220

City: Aalborg

Number of seats: