## News

## Second inspection session
Dear students, We notify you that the final grades of the re-exam are available on the website. The inspection session will happen this Tuesday in room 528 of E1 3, from 14:00 to 16:00.
Best regards, -- |

## Gentle reminder for the (re)examination
Dear students, Here are some informations about the re-exam, if you are registered, that should come as a recall: - The re-exam takes place this
**Tuesday 02.04.2019**, from**10:00 to 12:00** - The write-up duration is
**90min**, so the actual examination time will be**10:15 to 11:45**. - The exams… Read more
Dear students, Here are some informations about the re-exam, if you are registered, that should come as a recall: - The re-exam takes place this
**Tuesday 02.04.2019**, from**10:00 to 12:00** - The write-up duration is
**90min**, so the actual examination time will be**10:15 to 11:45**. - The exams are
**open-book,**which means you can bring any non-electronic document. This is due to the broad content of the lectures to be covered. - Don't forget to bring an ID card or other
**official**identification document.
Best regards and good luck! -- |

## Moved Room: 301. Examination results, and inspection date (Wednesday, 6 March)
Dear students, The results of Friday's exam are now published on the website, along with your grade. We have scheduled an inspection next week Wednesday afternoon, from 14:00 to 16:00, in 528, E 1 3. If you cannot make it at this date, you can… Read more
Dear students, The results of Friday's exam are now published on the website, along with your grade. We have scheduled an inspection next week Wednesday afternoon, from 14:00 to 16:00, in 528, E 1 3. If you cannot make it at this date, you can contact me to schedule another appointment.
Explanation about the results: because of the difficulty/length of the subject −sorry about this− we considered the last page (9points) of the last exercise, as bonus points, so passing the exam required 36 points instead of 45, over 90 points.
Best regards, -- |

## Examination informations
Dear students, Here are some informations about the examinations: - The first exam takes place this
**Friday, 22.02.2019**, the re-exam on**Tuesday 02.04.2019**, from**10:00 to 12:00** - The write-up duration is
**90min**, so the actual examination time would be**10:15 to 11:45**. - The exams are… Read more
Dear students, Here are some informations about the examinations: - The first exam takes place this
**Friday, 22.02.2019**, the re-exam on**Tuesday 02.04.2019**, from**10:00 to 12:00** - The write-up duration is
**90min**, so the actual examination time would be**10:15 to 11:45**. - The exams are
**open-book,**which means you can bring any non-electronic document. This is due to the broad content of the lectures to be covered. - Don't forget to bring an ID card or other
**official**identification document.
Extra office hour: if need by some of you, I can offer an extra office hour in the coming week. A poll in the forum is available to pick a date. Best regards, -- |

## Extra Office Hour this Monday
Dear students,
Due to several requests and since the room is still available, the tutors offer an additional office hour this Monday from 14:00 to 16:00 in the usual tutorial room.
Have a good evening and see you tomorrow for the last lecture ! -- |

## About Project2
Dear students, An important remark was reported by some of you: the persistence checking asks to give up the search as soon as a terminal state is found. This assumption is made in order to reject models that have terminal states. In the next question, the product of a system with a NBA of a LTL… Read more Dear students, An important remark was reported by some of you: the persistence checking asks to give up the search as soon as a terminal state is found. This assumption is made in order to reject models that have terminal states. In the next question, the product of a system with a NBA of a LTL formula may introduce new terminal states ! The NBA is indeed not assumed to be total, and some trace fragments may not have a corresponding run in the NBA. Please construct in this question a product system that This can be implemented in the following ways (non-exhaustive list):
I hope this extra specification clarifies the subject and makes the last question easier. Best, -- |

## Verification

**Audience**

This core lecture (Stammvorlesung) addresses Bachelor and Master students in *Computer Science, Bioinformatics, Embedded Systems, CuK or Computerlinguistics*. Bachelor students must have passed the base lecture *Programmmierung 1*. Decent knowledge in *Concurrent Programming * and *Theoretical Computer Science* is recommended.

**Contents**

The aim of this course is to introduce *Model Checking* and related automatic approaches to program verification. These techniques are especially suited for verifying properties of concurrent systems, systems which often comprise many nonterminating and communicating processes. We also review other verification techniques and domains.

Given a *mathematical model* of the system under consideration and a *property specification*, Model Checking examines all possible system states and checks if the specification is satisfied. The complexity of concurrent systems is due to the interleaving of the execution of the participating processes as well as to their interaction, for example by inter-process communication.

State-of-the-art model checking tools can handle state-spaces of about one billion distinguished states. Nevertheless, real-life systems may still exceed this limit by orders of magnitude. Therefore, techniques are needed which reduce this growth - known as the *state-space explosion problem* - without changing the (in-)validity of the specification's properties with respect to the original system-model.

The course is tentatively structured as follows:

- In the first part of this course, we study transition systems as a means of modelling reactive systems, discuss temporal logics, and look into computation tree logic (CTL) model checking.
- The second part introduces automata theory on infinite words, linear time temporal logic (LTL), and LTL model checking.
- In the third part, we address abstraction techniques and discuss model checking for timed systems, as well as other techniques for verification.