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 and Assoc. Prof. Rene Rydhof Hansen
ECTS: 2,5
Time: 12, 26 and 27 May, 2015
Place: Cassiopeia, Aalborg University, Selma Lagerlöfs Vej 300
Zip code: 9220
City: Aalborg
Number of seats:
Deadline: 29 April, 2015
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 and Assoc. Prof. Rene Rydhof Hansen
ECTS: 2,5
Time: 12, 26 and 27 May, 2015
Place: Cassiopeia, Aalborg University, Selma Lagerlöfs Vej 300
Zip code: 9220
City: Aalborg
Number of seats:
Deadline: 29 April, 2015
- Teacher: René Rydhof Hansen
- Teacher: Kim Guldstrand Larsen