Verification Bernd Finkbeiner

News

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