Verification Bernd Finkbeiner

News

02.10.2020

Re-exam: Check your registration status

Dear students,

the re-exam will take place in four weeks (October 29). By default, everyone who registered for the original re-exam date in March is registered for the new re-exam date as well. Please check your registration status in the LSF: Make sure to... Read more

Dear students,

the re-exam will take place in four weeks (October 29). By default, everyone who registered for the original re-exam date in March is registered for the new re-exam date as well. Please check your registration status in the LSF: Make sure to register if you want to take the exam but did not register for the original re-exam date in March. Make sure to deregister if you do not want to take the re-exam but registered for the original re-exam date. You can (de-)register until October 22. Note that you will find the re-exam registration in the LSF in the summer semester 2020 instead of the winter semester 2019/2020 due to technical problems. As soon as the grades are entered, the re-exam will be transferred back to the winter semester.

Your Verification Team

09.06.2020

Re-exam Registration

Dear students,

the registration for the re-exam in the LSF system is open again. Thus, you are now able to register or deregister.

Your Verification Team

 

19.05.2020

Re-exam scheduled

Dear students,

we have rescheduled the re-exam. It will take place on Thursday, October 29, at 10 am in lecture hall 002 in E 1 3.

The registration in the LSF system will be opened again. Hence, if you are already registered for the re-exam but do not want to... Read more

Dear students,

we have rescheduled the re-exam. It will take place on Thursday, October 29, at 10 am in lecture hall 002 in E 1 3.

The registration in the LSF system will be opened again. Hence, if you are already registered for the re-exam but do not want to take it anymore, you can unregister. If you are registered for the re-exam and still want to take it in October, you do not need to register again. If you did not register for the re-exam at March 17 but want to take it in October, you can register. 

If you have any questions or concerns, please let us know.

Your Verification Team

09.04.2020

Update Re-exam

Dear students,

This concerns those of you who registered for the re-exam in Verification. Due to the current situation, we do not know yet when the exam can take place. If you do not want to wait for the written exam, we can offer you to schedule an oral exam.... Read more

Dear students,

This concerns those of you who registered for the re-exam in Verification. Due to the current situation, we do not know yet when the exam can take place. If you do not want to wait for the written exam, we can offer you to schedule an oral exam. The exam would take place via a video conference. If you are interested, please let us know as soon as possible to find a suitable date. This is an additional offer, the written exam will still take place at a later date.

Stay healthy and happy Easter,

Your Verification Team

16.03.2020

Re-Exam Postponed

Dear Students,

Due to the current situation, we decided to postpone the exam scheduled for tomorrow (17.3.). We do not know yet when the exam can take place but we will let you know as soon as possible. If you have any questions or concerns, do not hesitate to... Read more

Dear Students,

Due to the current situation, we decided to postpone the exam scheduled for tomorrow (17.3.). We do not know yet when the exam can take place but we will let you know as soon as possible. If you have any questions or concerns, do not hesitate to ask.

Your Verification Team

12.03.2020

Re-exam and SARS-CoV-2

Dear students,

Please note the following remarks on the re-exam due to the current developments concerning the spread of the coronavirus SARS-CoV-2.

As matters stand now, the re-exam will take place as planned on Tuesday, March 17, at 2 pm in the Günter-Hotz... Read more

Dear students,

Please note the following remarks on the re-exam due to the current developments concerning the spread of the coronavirus SARS-CoV-2.

As matters stand now, the re-exam will take place as planned on Tuesday, March 17, at 2 pm in the Günter-Hotz lecture hall in building E 2.2.

However, you must not attend the re-exam if

  • you are infected,
  • your place of residence lies in the risk areas of coronavirus identified by the Robert Koch Institute,
  • you visited one of the risk areas of coronavirus identified by the Robert Koch Institute in the last 14 days,
  • you had contact with an infected person..

Please let us know via email if one of the above points applies to you. We will then find a solution together.

Since the re-exam will take place in a large lecture hall, we will be able to ensure the required distance of two arm lengths between students.

We are sorry for the inconveniences and we will make sure that this will not lead to any disadvantages for you.

Your Verification Team

06.03.2020

Re-exam Registration

Dear students,

we have entered the grades of the End-of-Term exam into the LSF system. Thus, if you want to participate in the re-exam on March 17, you are now able to register for it. Keep in mind that you have to register until March 10.

Your Verification Team

28.02.2020

Optional Project Results

Dear students,

the results of the optional project are now online. You can find them on your personal status page.

Your Verification Team

24.02.2020

End-of-Term Exam Inspection

Dear students,

the exam inspection will take place on Wednesday, March 4, from 2 pm to 4 pm, in seminar room 1.06 in E 1.1. Please bring your student ID.

Your Verification Team

21.02.2020

End-of-Term Exam Results

Dear students,

the results of the End-of-Term exam are now available on your personal status page in the rCMS.

We hope that you enjoyed the course and are looking forward to seeing you in upcoming lectures and seminars of the Reactive Systems Group. If you are... Read more

Dear students,

the results of the End-of-Term exam are now available on your personal status page in the rCMS.

We hope that you enjoyed the course and are looking forward to seeing you in upcoming lectures and seminars of the Reactive Systems Group. If you are interested in Bachelor/Master Theses or Research Immersion Labs, please contact us.

Your Verification Team

 

10.02.2020

Exam Information

Dear students,

Please note the following ahead of the exam next week on Tuesday, 18 February at 14:00pm. The exam will take place in lecture hall 0.01 (Günter-Hotz-Hörsaal) in E2 2. The re-exam will take place on 17 March. You need to pass either the exam or the... Read more

Dear students,

Please note the following ahead of the exam next week on Tuesday, 18 February at 14:00pm. The exam will take place in lecture hall 0.01 (Günter-Hotz-Hörsaal) in E2 2. The re-exam will take place on 17 March. You need to pass either the exam or the re-exam to pass the course.

The duration of the exams will be 150 minutes. They will be "open book", i.e., you are allowed to bring any hand-written or printed materials, including books, problem sets, and slides. Electronic devices such as e-book readers, smart watches, etc are not allowed.

You can pick up your problem sets and sample solutions for the exercise sheets during the additional office hour on Thursday (10:00 - 12:00) or at Jana's office (Room 1.15 in E1 1).

We wish you good luck for the exam!

Your Verification Team

29.01.2020

Optional Project - Deadline Extension

Dear Students,

upon request, we decided to extend the deadline of the optional project. You have time until February 6, 23:59, to finalize your submission.

For the competition, however, we will consider the last commit in your repository before the original... Read more

Dear Students,

upon request, we decided to extend the deadline of the optional project. You have time until February 6, 23:59, to finalize your submission.

For the competition, however, we will consider the last commit in your repository before the original deadline tomorrow.

Your Verification Team

15.01.2020

Typo in Definition of Method Merge

Dear students,

Unfortunately, there has been a typo in the definition of the method Merge in Problem 3 of Problem Set K. The first while loop in the definition of Merge has to loop until a.Length (not until l) to copy the whole array into mergea. We corrected... Read more

Dear students,

Unfortunately, there has been a typo in the definition of the method Merge in Problem 3 of Problem Set K. The first while loop in the definition of Merge has to loop until a.Length (not until l) to copy the whole array into mergea. We corrected the .pdf and the .txt files of the problem set. Thanks for pointing that out to us, we hope you enjoy working with Dafny now.

Your Verification Team

14.01.2020

Mandatory Project Results

Dear students,

the results of the mandatory project are now online. You can find them on your personal status page.

Your Verification Team

12.01.2020

Repositories Optional Project

Dear students,

We created new repositories for everyone who wants to participate in the optional project. You can find yours on the GitLab we used for the mandatory project. It is named groupXX_optional. The repository is empty, you will have to create your own... Read more

Dear students,

We created new repositories for everyone who wants to participate in the optional project. You can find yours on the GitLab we used for the mandatory project. It is named groupXX_optional. The repository is empty, you will have to create your own .gitignore file (depending on the programming language you use).

Please do not hesitate to ask if you have questions regarding libraries, the project specification, etc. We hope you enjoy the optional projects!

Your Verification Team

 

09.01.2020

Evaluation and Optional Project

Dear students,

the course evaluation will take place in the lecture on Tuesday, January 14. We are looking forward to getting your feedback!

 

Furthermore, the optional project will start on Monday, January 13. If you want to participate in the project,... Read more

Dear students,

the course evaluation will take place in the lecture on Tuesday, January 14. We are looking forward to getting your feedback!

 

Furthermore, the optional project will start on Monday, January 13. If you want to participate in the project, please upload a text file on your personal status page until Saturday, January 11, 23:59 with the names and matriculation numbers of all of your group members. The maximal group size is 2. It is sufficient to upload one text file for each team.

Shortly after the registration, we will grant you access to a new GitLab repository. We will freeze your old repository after today's deadline of the mandatory project, so you cannot keep working there. We recommend to copy over your code from the mandatory project if you want to extend it.

More information can be found in the project description in the materials sections.

 

Your Verification Team

 

 

11.12.2019

Problem Set H: Zeno Timed Automaton in H1

Dear students,

We have been made aware that the timed automaton given in exercise H1 of Problem Set H is Zeno while we defined Region Graphs only for non-Zeno timed automata. We have uploaded a new version of the Problem Set where we removed the loops in states... Read more

Dear students,

We have been made aware that the timed automaton given in exercise H1 of Problem Set H is Zeno while we defined Region Graphs only for non-Zeno timed automata. We have uploaded a new version of the Problem Set where we removed the loops in states s1 and s2 in order to make the timed automaton non-Zeno.

If you already constructed the Region Graph for the timed automaton given in rev 1 although it was Zeno, you may hand in this solution. Otherwise, use the timed automaton given in rev 2. Please point out in your solution which timed automaton you used.

We are sorry for the confusion!

Your Verification Team

18.11.2019

Mandatory Project Part 1

Dear students,

the first part of the mandatory project is online. You may find the project description in the materials section.

We have granted you access to your team’s repository in the GitLab of the CS department of the university. The code template for... Read more

Dear students,

the first part of the mandatory project is online. You may find the project description in the materials section.

We have granted you access to your team’s repository in the GitLab of the CS department of the university. The code template for the project is contained in the repositories.

Important: If you did not register in the GitLab so far, do so as soon as possible. The later you register, the more your access to the code template will be delayed.

Have fun with the project!

Your Verification Team

14.11.2019

Project Repositories

Dear students,

for the project, we will provide a GitLab repository for each team in the GitLab of the Computer Science faculty. The code template will be already contained in the repository. In order to give you access to your repository, you have to login into... Read more

Dear students,

for the project, we will provide a GitLab repository for each team in the GitLab of the Computer Science faculty. The code template will be already contained in the repository. In order to give you access to your repository, you have to login into the faculty GitLab (using the Student-Employee-LDAP):

https://gitlab.cs.uni-saarland.de/

If you don't remember your password for the faculty services of the Computer Science faculty, you can use the following link to reset your password (notice that it can take some time until you receive an e-mail to reset your password).

https://udo.cs.uni-saarland.de/pw/requestpwd.php

After your successful login, you have an account there, which we can add to your team’s repository afterwards and hence grant you access.

Your Verification Team

13.11.2019

Problem Set D Wrong Hint

Dear students,

We have been made aware that the hint given in exercise D2 a) of Problem Set D is wrong. In order to make the NBAs non-blocking, you will need four states for Aand three states for A2. We are sorry for the confusion!

Your Verification Team

12.11.2019

Project Team Registration

The project will start on Monday Nov 18. The workload of the project is designed for groups of two people. Hence, please upload a text file until Thursday Nov 14 on your personal status page including your and your teammates matriculation number and name. It is... Read more

The project will start on Monday Nov 18. The workload of the project is designed for groups of two people. Hence, please upload a text file until Thursday Nov 14 on your personal status page including your and your teammates matriculation number and name. It is sufficient to upload one text file for each team.

While you may also do the project on your own, we strongly recommend to get in touch with your classmates to find a teammate.

31.10.2019

Results Problem Set A

Dear Students,

We finished grading Problem Set A, you can find your points on your Personal Status Page. The sheets you handed in can be collected in the Office Hours or during the Tutorials next week.

Your Verification Team

 

25.10.2019

Tutorial Assignment

Dear students,

the tutorial slots have been assigned. Please refer to your personal status page for further information on your tutorial.

Your Verification Team

15.10.2019

Dates and Times

Dear students,

Welcome to Verification!

We have two small corrections regarding dates and times: First, we had to move the time slot for our office hour. The office hour will take place Mondays, 1pm - 3pm (not 2pm - 4pm). Second, other than written on the... Read more

Dear students,

Welcome to Verification!

We have two small corrections regarding dates and times: First, we had to move the time slot for our office hour. The office hour will take place Mondays, 1pm - 3pm (not 2pm - 4pm). Second, other than written on the slides today, the first assignment will be handed out next Tuesday after the lecture. It is due Tuesday the week after, before the lecture starts. The slides will be updated accordingly.

Looking forward to the coming semester,

Your Verification Team

Show all
 

Verification

Core Lecture Course (9 CP)

Lectures: Tuesday 2-4 pm and Thursday 10-12 am in HS001, E1.3.
Tutorials: Wednesday 10-12 am or 2-4 pm in E1.1, Room 1.06.
Office Hours: Monday 1-3pm in E1.1, Room 1.06

 

Syllabus

How can one ensure that computer programs actually do what they are intended to do? Simply running a program repeatedly with various inputs is inadequate, because one cannot tell which inputs might cause the program to fail. It is possible to tailor a tester to test a given program, but present-day programs are so complex that they cannot be adequately checked through conventional testing, which can leave significant bugs undetected. Program verification uses mathematical and logical methods to prove that a program is correct. This approach was pioneered by, among others, Dijkstra, Floyd, Gries, Hoare, Lamport, Manna, Owicki and Pnueli. Today, we have powerful decision procedures that can, completely automatically, answer basic questions about the data types typically used by programmers. Model Checking is a “push-button” technology that can analyze finite-state abstractions of programs with as many as 1020 states. This course takes an up-to-date look at the theory and practice of program verification.

 

Main Textbooks

  • Christel Baier, Joost-Pieter Katoen: Principles of Model Checking, 2008
  • Aaron R. Bradley and Zohar Manna: The Calculus of Computation (online version available through Springer Link).

 

Recommended Reading

  • Temporal Verification of Reactive Systems – Safety by Zohar Manna and Amir Pnueli, Springer Verlag, ISBN: 0387944591
  • Model Checking by Edmund M. Clarke, Jr., Orna Grumberg and Doron A. Peled, MIT Press; ISBN: 0262032708
  • Krystof R. Apt, Frank S. de Boer, Ernst-Rüdiger Olderog: Verification of Sequential and Concurrent Programs, 2009

 

 

 

 



Privacy Policy | Legal Notice
If you encounter technical problems, please contact the administrators