Verification Holger Hermanns, Daniel Stan

News

27.11.2018

Project phase 1 and misc

Dear students,

 

You may have noticed some bugs in the template project available in the source material, thank you for reporting these. An updated revision has just been uploaded to the material section. Due to some requests, the project template can also be... Read more

Dear students,

 

You may have noticed some bugs in the template project available in the source material, thank you for reporting these. An updated revision has just been uploaded to the material section. Due to some requests, the project template can also be retrieved as a git repository at this adress:
https://dgit.cs.uni-saarland.de/dstan/muds-project
(NB: a registration with your uds mail account may be necessary). 

The new revision include two types of improvement (see README.md): parsing of the input models (add support for integer parenthesis) and fixes of sample files (missing ; and some parenthesis missing for some temporal formulae). 

These errors should not affect your implementation, nor the final testing/grading, since this procedure will consists in calling each of the implemented method with several input parameters. Nonetheless, you may still be interested in this update in order to test your implementation, my apologies for the inconvenience.

I recall that this first part of the project is due on Monday 10th december.

By this news entry, I also notify you that the last "mini-test" grades have been released, as long as the correction of last week's exercise sheet sample solutions and the weekly exercise sheet −about  ω-regular languages− enjoy !

As always, feel free to ask any question during our weekly office hours, on Thursday, or during the tutorials, or on the forum !

 

Cordially,

-- 
Daniel STAN

15.11.2018

Office Hours are moving downstairs (SR 107 in E1 3)

Dear students,

As you may have noticed on the schedule, our office hour has been affected a bigger room, same time.

The new room is SR 107 in E1 3, still every Thursday (today too) from 10:00 to 12:00 and 14:00 to 16:00.

 

During today office hours, you... Read more

Dear students,

As you may have noticed on the schedule, our office hour has been affected a bigger room, same time.

The new room is SR 107 in E1 3, still every Thursday (today too) from 10:00 to 12:00 and 14:00 to 16:00.

 

During today office hours, you will be able to work and ask questions on the training exercise sheets, and also ask to consult your minitest sheet.

See you there !

--
Daniel

06.11.2018

Training sheet C went online

Dear students,

This week's training sheet has been uploaded in the corresponding materials section. These documents contain exercises you can use to check and train your understanding of the last week lectures. We remind you that office hours will take place on... Read more

Dear students,

This week's training sheet has been uploaded in the corresponding materials section. These documents contain exercises you can use to check and train your understanding of the last week lectures. We remind you that office hours will take place on thursday (see timetable for exact hours and location), and that you can use this time slot for questions regarding the current or previous training sheets.

As a courtesy, we also uploaded sample solutions (without guarantee it will still be provided in the future !) for the two previous training sheets.

Enjoy !

--
Daniel STAN

29.10.2018

Tutorial assignements went online

Dear students,

Due to a mis-understanding in how dcms works, assignements to tutorial sessions have been delayed. The situation is now fixed and you can see which tutorial schedule you have been assigned to.

Because of the late announcement, you are still... Read more

Dear students,

Due to a mis-understanding in how dcms works, assignements to tutorial sessions have been delayed. The situation is now fixed and you can see which tutorial schedule you have been assigned to.

Because of the late announcement, you are still allowed to attend the other tutorial session *this week* if you cannot do otherwise.

My apologies for the misunderstanding,

-- 
Daniel STAN

 

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.


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