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.
Format:
Lectures and exercises.
Organizer: Prof. Kim G. Larsen <kgl@cs.aau.dk> and Assoc. Prof. Rene Rydhof Hansen <rrh@cs.aau.dk>
Lecturers: Prof. Kim G. Larsen <kgl@cs.aau.dk> and Assoc. Prof. Rene Rydhof Hansen <rrh@cs.aau.dk>
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:
Deadline:
- Teacher: Kim Guldstrand Larsen