Verification

Bernd Finkbeiner

News

Re-exam inspection

Written on 24.04.24 by Arthur Correnson

Dear all, The re-exam inspection will take place on Thursday, May 2, from 10 am to 11 am, in seminar room SR 1.06 in building E1 1. Please bring your student ID. Cheers!

Results of Re-Exam

Written on 21.03.24 by Bernd Finkbeiner

Dear All, we have published the results of the Re-Exam. You can find your result on the Personal Status page. Have a nice remaining semester break!

Your Verification Team

Re-exam

Written on 07.03.24 by Arthur Correnson

Dear all,

We just uploaded the grades for the final exam on LSF; students who want to participate in the re-exam can now register!

Cheers,
The Verification Team.

Exam inspection

Written on 23.02.24 by Bernd Finkbeiner

Dear all, The exam inspection will take place on Thursday, February 29, from 10 am to 11 am, in seminar room SR 206 in building E1 1. Please bring your student ID. Cheers!

Exam results

Written on 14.02.24 by Bernd Finkbeiner

Dear all, the results of today's exam are available online. Have a nice evening, happy Valentine's Day, good luck with any other exams, and (very soon) a great semester break!

Exam

Written on 12.02.24 by Arthur Correnson

Hi all,

Just a reminder that the final exam for Verification will be on Wednesday the 14th in Günter-Hotz-Hörsaal at 10 am.
The exam will be exactly 120 minutes. Please arrive at 10:00 and don't forget to bring your student ID.
Also, remember that the exam is open-book so feel free to bring any… Read more

Hi all,

Just a reminder that the final exam for Verification will be on Wednesday the 14th in Günter-Hotz-Hörsaal at 10 am.
The exam will be exactly 120 minutes. Please arrive at 10:00 and don't forget to bring your student ID.
Also, remember that the exam is open-book so feel free to bring any printed material you'd like (using electronic devices will be forbidden).

Good luck preparing for the exam!
See you all on Wednesday.

Cheers,
The Verification Team


 

Solution to Problem Set 14

Written on 08.02.24 by Arthur Correnson

Hello all,

Multiple news:

1) We just released solutions for problem set 14 (the one to prepare for the exam)

2) Remember that Monday 12, at 10am we will have an office hour in Lecture Hall 2.
Attendance is not mandatory, but feel free to join if you have any questions before the exam!
Note… Read more

Hello all,

Multiple news:

1) We just released solutions for problem set 14 (the one to prepare for the exam)

2) Remember that Monday 12, at 10am we will have an office hour in Lecture Hall 2.
Attendance is not mandatory, but feel free to join if you have any questions before the exam!
Note that the building will not be open before 9:30 because Monday is a holiday.

Cheers,
The Verification Team.


 

Minitests + Additional Problem Set

Written on 06.02.24 by Arthur Correnson

Dear all,

The grades for today's minitest are online.
We also released an additional problem set to help you prepare for the exam.

Cheers,
The Verification Team.
 

Please register for the exam!

Written on 02.02.24 by Bernd Finkbeiner

Dear all, here is some information about our upcoming exam, as discussed in today's lecture:

  • Important: Please register for the exam. The registration deadline is one week before the exam, on February 7.
  • Please check your CMS status page to see if you have reached the necessary number of… Read more

Dear all, here is some information about our upcoming exam, as discussed in today's lecture:

  • Important: Please register for the exam. The registration deadline is one week before the exam, on February 7.
  • Please check your CMS status page to see if you have reached the necessary number of points in the minitests (at least 50% of 120 points, i.e., at least 60 points).
  • We recommend registering for the exam right now, even in case you are still missing a few points. At the last minitest (#13) on Tuesday, your points will count as bonus points (i.e., they count for reaching the threshold, but do not increase the threshold).
  • There will be one more problem set next week, with exercises that will help you to prepare for the exam.
  • We plan to offer an optional office hour on Monday, February 12 (Rosenmontag), starting at 10 am. (Room to be announced.) 
  • The exam will be on Wednesday, February 14, 2024, starting at 10 am. The exam will take two hours and will be open-book. Bring any notes or printed materials you like. 

In case you have any questions or concerns, please let us know. Have a great weekend, and see you on Tuesday!

Lecture on Friday ONLINE only

Written on 31.01.24 by Bernd Finkbeiner

Dear all, As you are probably aware, the bus drivers in Saarbrücken are expected to be on strike this Friday. We will therefore meet online for Friday's lecture. Please join the Zoom meeting at the link given under "Zoom" on the Materials page. The tutorial on Thursday will take place in person as… Read more

Dear all, As you are probably aware, the bus drivers in Saarbrücken are expected to be on strike this Friday. We will therefore meet online for Friday's lecture. Please join the Zoom meeting at the link given under "Zoom" on the Materials page. The tutorial on Thursday will take place in person as usual. See you soon!

Problem Set 13

Written on 31.01.24 by Bernd Finkbeiner

Dear all, Problem Set 13 and the results of yesterday's minitest are available online. Cheers! 

Problem Set 12

Written on 24.01.24 by Arthur Correnson

Dear all,
Problem set 12 is now available. The grades from yesterday's minitest are also online.

Cheers,
The Verification Team.

Solutions for Problem Set 10

Written on 19.01.24 by Bernd Finkbeiner

Dear All, Since some of you could not attend the tutorial this week because of the bad weather, our wonderful tutors kindly wrote up the solutions for Problem Set 10. Please find the Solution Set on the "Materials" page. Thank you, Angelina, Vladimir, and Mihir! Have a great weekend, everyone! 

Problem Set 11, course evaluation

Written on 16.01.24 by Bernd Finkbeiner

Dear All, Problem Set 11 and the results of today's minitest are now online. If you have not yet had a chance to fill out the course evaluation, please be sure to visit the links to the qualis website, which are available in the Materials section: we are excited to hear whether you liked the course!… Read more

Dear All, Problem Set 11 and the results of today's minitest are now online. If you have not yet had a chance to fill out the course evaluation, please be sure to visit the links to the qualis website, which are available in the Materials section: we are excited to hear whether you liked the course! Thanks a lot for your time and effort, your comments are highly appreciated.

Tutorial tomorrow ONLINE only

Written on 16.01.24 by Bernd Finkbeiner

Dear all, Due to the potentially dangerous weather conditions tomorrow, the Wednesday tutorial will take place online. Please join the Zoom meeting at the link given under "Zoom" on the Materials page. Alternatively, you are also welcome to attend the tutorial on Thursday instead. We expect that the… Read more

Dear all, Due to the potentially dangerous weather conditions tomorrow, the Wednesday tutorial will take place online. Please join the Zoom meeting at the link given under "Zoom" on the Materials page. Alternatively, you are also welcome to attend the tutorial on Thursday instead. We expect that the tutorial on Thursday will take place in person as usual.

Room change for lecture today: HS 003

Written on 09.01.24 by Bernd Finkbeiner

Dear all, Please note that today's lecture will be in E 1.3 HS 003 instead of our usual HS 001. The reason for the change is that the lecture from the other room needs the audio equipment that is only available in "our" lecture hall. The room change is for today only, we'll be back in HS 001 on… Read more

Dear all, Please note that today's lecture will be in E 1.3 HS 003 instead of our usual HS 001. The reason for the change is that the lecture from the other room needs the audio equipment that is only available in "our" lecture hall. The room change is for today only, we'll be back in HS 001 on Friday. See you at 2 pm!

Problem Set 9

Written on 20.12.23 by Arthur Correnson

Dear all,

Problem set 9 is online, as well as the results of Tuesday's minitest.

Cheers,
The Verification team.

No lectures on Dec 22 and Jan 2

Written on 15.12.23 by Bernd Finkbeiner

Dear all,

Since many of us will not be in Saarbrücken on Friday, Dec 22, and Tuesday, Jan 2, we decided to cancel the two lectures. So the last lecture before the Christmas break will be on Tuesday, Dec 19, and the first lecture in the new year will be on Friday, Jan 5. (There will be a minitest on… Read more

Dear all,

Since many of us will not be in Saarbrücken on Friday, Dec 22, and Tuesday, Jan 2, we decided to cancel the two lectures. So the last lecture before the Christmas break will be on Tuesday, Dec 19, and the first lecture in the new year will be on Friday, Jan 5. (There will be a minitest on Dec 19 and then again on Jan 9.)

Have a great weekend, and see you on Tuesday!

Problem Set 8 + Minitests

Written on 12.12.23 by Arthur Correnson

Dear all,

The results of today's minitest and the new problem set are online!

Cheers,
The Verification team

Minitest 6 + Problem Set 7

Written on 05.12.23 by Bernd Finkbeiner

Dear all,

The results of today's minitest and the new problem set are online!

Cheers,
The Verification team

Minitest 5 + Problem set 6

Written on 28.11.23 by Arthur Correnson

Dear all,

The results of today's mini-tests and the new problem set are online!
Have a nice evening ;)

The verification team.

Problem Set 5 + Minitests

Written on 21.11.23 by Arthur Correnson

Dear all,

The results of minitest 4 are now published.
We also released the new problem set.

As always, if you have any questions, do not hesitate to email us!

The Verification team.

Problem set 4 + Results of the minitest

Written on 14.11.23 by Arthur Correnson

Dear all,

The results of minitest 3 are now published.
We also released the new problem set.

As always, if you have any questions, do not hesitate to email us!

The Verification team.

Tutorial Room

Written on 08.11.23 by Arthur Correnson

Dear all,

The tutorial room is E1.1 1.06 (and not E1.3, as was written in the timetable....).
Sorry for the confusion...

 

Results of the minitests + Problem set 3

Written on 07.11.23 by Arthur Correnson

Dear all,

The results of the second minitest are now published.
We also released the third problem set.

Remember that tutorials start this week; we will start tomorrow with group A.
As always, if you have any questions, do not hesitate to email us!

The Verification team.

Tutorial Assignment

Written on 07.11.23 by Arthur Correnson

Dear all,

We just assigned everybody to a tutorial slot.
You can see your assigned tutorial on your personal status page.

See you at 2:15 for the lecture!

The Verification team.


 

Results of the minitest + Problem set 2

Written on 31.10.23 by Arthur Correnson

Dear all,

The results of the first minitest are now published.
We also released the second problem set.

Remember that there will be no tutorial this week; we will start only next Wednesday.
If you have any questions regarding the second problem set, do not hesitate to send us an email!

Have… Read more

Dear all,

The results of the first minitest are now published.
We also released the second problem set.

Remember that there will be no tutorial this week; we will start only next Wednesday.
If you have any questions regarding the second problem set, do not hesitate to send us an email!

Have a nice holiday!
The Verification team.

Tutorial Registration

Written on 25.10.23 by Arthur Correnson

Dear all,

We just opened the registration for tutorials.
Please select your preferred tutorial slot on your personal status page by November 1st.
The tutorials will start on November 8th.

The Verification team.

First Problem Set

Written on 24.10.23 (last change on 25.10.23) by Arthur Correnson

Dear all,

We just released the first problem set of the semester! You can find it on the Materials page.
You do not need to hand in any solution, but we strongly recommend that you look at the problems.
There will be no tutorial this week, but we will have a mini-test on Tuesday (the 31st of… Read more

Dear all,

We just released the first problem set of the semester! You can find it on the Materials page.
You do not need to hand in any solution, but we strongly recommend that you look at the problems.
There will be no tutorial this week, but we will have a mini-test on Tuesday (the 31st of October).
The mini-test will be in the spirit of the questions of the problem set.

If you have any questions regarding the content of the problem set, do not hesitate to send an email to arthur.correnson@cispa.de !
We will discuss this problem set in more detail in the second week of November.
 

See you all on Friday,
The verification team.
Show all

Verification

Core Lecture Course (9 CP)
Lectures Tuesdays 2:15 to 4 pm and Fridays 10:15 am to 12 noon in HS001, E1 3.

 

Syllabus

Computers and programs are everywhere, including in critical places where human lives are at stake (airplanes, hospitals, nuclear power plants, ...). In this context, how can one ensure that computer programs do what they are intended to do without harming humans?

To answer this question, one could stress-test the robustness of programs by running them repeatedly with various inputs to identify which might cause a failure. This solution is unsatisfactory because the input spaces can be unreasonably large, and testing all scenarios is simply out of reach. It is possible to tailor a tester to test a given program, but present-day programs are so complex that traditional testing techniques can leave significant bugs undetected.

Another approach is to prove, once and for all, that programs are correct using mathematical and logical methods. This approach was pioneered by, among others, Dijkstra, Floyd, Gries, Hoare, Lamport, Manna, Owicki, and Pnueli. Their research led to the development of an extensive array of techniques to establish, formally, the conformance of programs to a given specification. Today, these techniques have evolved into powerful verification tools that can automatically prove the correctness of large programs.

Model Checking is one of these "push-button" verification technologies. Given a program and a specification, a model checker can automatically verify that the program is correct or identify a scenario where it fails to satisfy its specification. This course takes an up-to-date look at the theory and practice of program verification using model-checking methods.

 

Recommended Reading

  • Christel Baier, Joost-Pieter Katoen: Principles of Model Checking, 2008.
  • Edmund M. Clarke, Orna Grumberg, Daniel Kroening, Doron Peled, Helmut Veith: Model Checking, 2018.
  • Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, Roderick Bloem: Handbook of Model Checking, 2018 (available on Springer Link).
  • Aaron R. Bradley and Zohar Manna: The Calculus of Computation, 2007 (available on Springer Link).
Privacy Policy | Legal Notice
If you encounter technical problems, please contact the administrators.