Fundamentals of Model Checking and Static Analysis (2013)

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.

Organizer:
Professor Kim G. Larsen, email: kgl@cs.aau.dk
Associate Professor Rene Rydhof Hansen, email: rrh@cs.aau.dk

Lecturers:
Professor Kim G. Larsen, email: kgl@cs.aau.dk
Associate Professor Rene Rydhof Hansen, email: rrh@cs.aau.dk

ECTS:
2.5

Time:
8-10 course sessions in April/May 2013:
Wed 03 APR 2013 - room 0.2.11
Wed 12 APR 2013 - room 0.2.12
Wed 17 APR 2013 - room 0.2.11
Wed 24 APR 2013 13:00-16:00 - room 0.2.11
Thur 25 APR 2013 13:00-16:00 - room 0.2.11
Wed 01 MAY 2013 - room 0.2.11
Tue 07 MAY 2013 - room 0.2.11
Tue 14 MAY 2013 - room 0.2.11
Tue 21 MAY 2013 - room 0.2.11
Mon 16 SEP 2013 13:00-16:00 - room 0.2.11
Tue 17 SEP 2013 13:00-16:00 - room 0.2.12


Place:
Aalborg University

Zip code:
9220

City:
Aalborg

Number of seats:

Deadline:
March 1, 2013

Important information concerning PhD courses
We have over some time experienced problems with no-show for both project and general courses. It has now reached a point where we are forced to take action. Therefore, the Doctoral School has decided to introduce a no-show fee of DKK 5,000 for each course where the student does not show up. Cancellations are accepted no later than 2 weeks before start of the course. Registered illness is of course an acceptable reason for not showing up on those days. Furthermore, all courses open for registration approximately three months before start. This can hopefully also provide new students a chance to register for courses during the year. We look forward to your registrations.