Verification Bernd Finkbeiner

News

23.03.2017

Re-exam and Project Bonus

Dear students,

the re-exam takes place on April 3 at 10:00 in HS002 in E1.3 and optionally HS003 in E1.3 (not in the mathematics building this time). If you would like to participate in the re-exam, please register until Monday, March 27 in the LSF. Please bring... Read more

Dear students,

the re-exam takes place on April 3 at 10:00 in HS002 in E1.3 and optionally HS003 in E1.3 (not in the mathematics building this time). If you would like to participate in the re-exam, please register until Monday, March 27 in the LSF. Please bring your student ID and please keep in mind that the re-exam will be open book as well.

If you worked on the optional project, you may check your personal status page to see which bonus you received.

06.03.2017

Exam Inspection

Dear students,

the exam inspection will be on Friday, March 10, at 2pm in SR106 in E1.1. Please bring your student ID.

28.02.2017

Exam Results

Dear students,

the results of the final exam are available in the rCMS.

21.02.2017

Exam Information

Dear students,

the exam will take place on Thursday, 23, at 1pm in HSI E2.5 and HSII E2.5. Please make sure to be there no later than 12:50, so that we can start in time.

Students with last names from A to M will write in HSI and students with last names from... Read more

Dear students,

the exam will take place on Thursday, 23, at 1pm in HSI E2.5 and HSII E2.5. Please make sure to be there no later than 12:50, so that we can start in time.

Students with last names from A to M will write in HSI and students with last names from N-Z will write in HSII. There will be no further seating arrangement.

Please keep in mind that the exam is open book.

15.02.2017

IC3 competition @ final lecture tomorrow

Dear students,

we've almost reached the end of the verification course -- thank you all for participating so actively, it has been great to work with all of you!

In our final lecture on Thursday, we will host a competition between the IC3-based model checkers... Read more

Dear students,

we've almost reached the end of the verification course -- thank you all for participating so actively, it has been great to work with all of you!

In our final lecture on Thursday, we will host a competition between the IC3-based model checkers that have been submitted as an optional project. We've prepared a small surprise for the winning group. So if you think it could be you, please attend!

All the best,
Bernd Finkbeiner, Christopher Hahn, Norine Coenen, Paul Gölz, Maximilian Schwenger, and Leander Tentrup

03.02.2017

Exams

We fixed the date for the re-exam to April 3, 10:00 am. The end term exam will be on February 23 at 1:00 pm. The duration of our exams will be 150 minutes. The exams will be "open book", i.e., you are allowed to access any hand-written or printed materials you bring... Read more

We fixed the date for the re-exam to April 3, 10:00 am. The end term exam will be on February 23 at 1:00 pm. The duration of our exams will be 150 minutes. The exams will be "open book", i.e., you are allowed to access any hand-written or printed materials you bring to the exam, including books, problem sets and slides. Electronic devices are prohibited.

Please make sure to register in time in the LSF. An additional registration in the rCMS is not needed.

17.01.2017

Optional Project

The description for the optional project is now available in the materials section. If you would like to participate (and earn up to 0.7 bonus to your grade), please send an email to Maximilian (schwenger@stud.uni-saarland.de) until Jan 19, 6pm containing the names... Read more

The description for the optional project is now available in the materials section. If you would like to participate (and earn up to 0.7 bonus to your grade), please send an email to Maximilian (schwenger@stud.uni-saarland.de) until Jan 19, 6pm containing the names of every member in your group. The maximal group size is two.

12.01.2017

Project Results

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

13.12.2016

Block Seminar: Runtime Verification

Dear Students,

We are offering a block seminar on Runtime Verification. Runtime verification is a dynamic analysis method, where an execution of a system is checked during runtime against a specification. 

The seminar is a two week seminar that will take place... Read more

Dear Students,

We are offering a block seminar on Runtime Verification. Runtime verification is a dynamic analysis method, where an execution of a system is checked during runtime against a specification. 

The seminar is a two week seminar that will take place in March. The registration is open until Thursday, December 22nd. For more information please visit the course's page or contact Hazem Torfah

06.12.2016

Project Part 3

The third part of our project is now online. You may find the project handout in the materials section.

29.11.2016

Project Part 2

The second part of our project is now online. You may find the project handout in the materials section.

22.11.2016

Project Part 1

The first part of our project is now online. You may find the project handout in the materials section.
Important: Please register as soon as possible at https://version.react.uni-saarland.de with the same email address you used in the rcms.
If you register until... Read more

The first part of our project is now online. You may find the project handout in the materials section.
Important: Please register as soon as possible at https://version.react.uni-saarland.de with the same email address you used in the rcms.
If you register until 4pm, we will assign you as soon as possible to your project repository and hence grant you access to the code template.
Otherwise, your access to the project might be delayed.

Have fun with the project!

17.11.2016

Project Team Registration

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

The project will start on Tuesday Nov 22. The workload of the project is designed for groups of two people. Hence, please upload a text file until Monday Nov 21 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 you to get in touch with your classmates in the forum to find a teammate.

04.11.2016

Tutorial Assignment

We have assigned the tutorial slots. You may find your slot on your personal status page.
 

26.10.2016

Additional Tutorial Slot

Due to some time collisions, we now offer a third tutorial on Wednesdays 12 noon. You may choose between the following time slots on your personal status page until Nov 3:
Monday 10-12
Monday 12-14
Wednesday 12-14

If you have any problems regarding the... Read more

Due to some time collisions, we now offer a third tutorial on Wednesdays 12 noon. You may choose between the following time slots on your personal status page until Nov 3:
Monday 10-12
Monday 12-14
Wednesday 12-14

If you have any problems regarding the organization of the course, please write an email to hahn@react.uni-saarland.de or use the forums.

13.09.2016

Registration

Registration is now open till Thursday, the 3rd of November.

Show all
 

Verification

Core Lecture Course (9 CP)

Tuesday 10-12 am and Thursay 4-6 pm in HS002, E1.3.

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


If you encounter technical problems, please contact the administrators