News

Semantics & Verification, Spring 2005

---

• June 5th, 2005.
  The syllabus (pensum) information for the exam can be found on Course Info web-page. I will be out of Denmark from June 16th until the exam start. I won't be able to answer your questions (not even email queries) durig this period. You are adviced to ask any questions directed to me before this date, after June 16th try to contact Bjørn.
  
  
• May 2nd, 2005.
  Reports accepted for the second mini project are listed here. Verify that your student number is on the list and notify the lecturer about possible inconsistences. If your number is not on the list, you will not be given pensum dispensation for the corresponding question "Gossiping girls problem and its modelling and verification using UPPAAL".
  
  
• April 26th, 2005.
  
  • Please, note that the deadline for the second mini project is Friday, April 29th. Remember to check the web-page in the middle of the next week to see whether your second mini project was accepted (students' numbers will be listed similarly as in the first mini project).
  • A detailed list of exam questions is now available here.
  
  
  
• April 21st, 2005.
  Even though there is no miniproject concerning BDDs, you can have a look at the tool IBEN for manipulation with BDDs. We will be using the tool in the last tutorial (Tutorial 14). Iben can be run e.g. from the command line on borg (/pack/FS/pack/iben-1.1/bin/iben) and it is extremely easy to use. Here is a very short manual and a small demo:
  
  iben> vars x y (This declares two boolean variables x (the 0th variable) and y (the first variable))
  iben> satisfy x & y
  <0:1, 1:1> (This says that the only satisfying assignment is one in which the 0th variable, namely x, is true, and so is the first one, namely y.)
  iben> vars z (This declares the variable z with index 2)
  iben> satisfy x & y & !z
  <0:1, 1:1, 2:0>
  iben> satisfy x + (!x & y & !z)
  <0:0, 1:1, 2:0><0:1> (This says that there are two families of satisfying assignments. In the second one, the only thing that matters is that x is true.)
  iben> show x + (!x & y & !z) (This shows the resulting ROBDD as a postscript file.)
  
  
• April 14th, 2005.
  If you have a question about your first mini project or would like to clarify some of your answers, I will be in my office B2-203 on Friday (April 15th) between 13:00 and 14:30. You are very welcome to drop by. Please, bring a printed copy of your pdf mini report.
  
  
• April 13th, 2005.
  Reports accepted for the first mini project are listed here. Verify that your student number is on the list and notify the lecturer about possible inconsistences. If your number is not on the list, you will not be given pensum dispensation for the corresponding question about "Alternating bit protocol and its modelling in CWB".
  
  
• April 7th, 2005.
  
• Information about the second mini project is now available here.
  
  
• April 5th, 2005.
  The deadline for the first mini project is April 7th (midnight). During the weekend, you may wish to install UPPAAL (www.uppaal.com) on your laptops, read one of the UPPAAL tutorials available on-line and play little bit with the examples provided in the folder "demo". The second UPPAAL mini project will be available on the web-pages soon.
  
  
• March 30th, 2005.
  Lectures plan has been updated. The tutorial classes on Monday (April 4th) will be used to finalize the first mini project and to write down a short report.
  
  
• March 17th, 2005.
  I have recently noticed that some of you already started to prepare the report concerning the first mini project. Please, consider this not as a regular report but rather as a documentation that you did your work. Copy and paste of the source code with very short comments (possibly included in the code), an itemized list of your verification resutls and one paragraph of a conclusion is more than sufficient! All this can be written on two or at most three pages. Such mini projects (provided that the code looks reasonable) will be accepted without any problems.
  
  
• March 16th, 2005.
  I am travelling (out of Denmark) until March 30th. I will be probably very slow in answering emails, so in case you need some assistance concerning the course or the mini project you might consider contacting Bjørn (office B2-205).
  
  
• March 7th, 2005.
  On Wednesday (9.3.2005) at 8:15 starts the 4 hour block dedicated to solving the first mini project. The morning will start with a quick information about the mini project. Remember to make sure that you can run CWB on your laptop and bring any literature you might find useful. We will be available in the lectureroom until 12:00 to answer your questions.
  
  
• March 6th, 2005.
  There is a new (and very short) note called Game Characterization of Hennessy-Milner Logic with One Recursively Defined Variable available from the on-line material. Typos found in this note count into the competition for the best reader and I would be very grateful if you read the note carefully and let me know about any problems you might find there.
  
  
• February 27th, 2005.
  Lectures plan has been updated. Pay a special attention to the unusual room location of the Wednesday's lecture. The description of the first mini-project is now available here.
  
  
• February 16th, 2005.
  Solutions to exercise set 4 are on-line. There won't be any lectures or tutorials for the next two weeks. You are adviced to play with CWB in your leasure time (and try to install it on your computer if you wish so) and if you give me your solution to Exercise 7 (tutorial 4) in written, I will correct it for you.
  
  
• February 14th, 2005.
  The typos on the slides from Lecture 4 are fixed and the slides are now available from the usual location. The solutions to exercise set 3 are also on-line.
  
  
• February 12th, 2005.
  The slides will be now available before lectures. Please, consider them as preliminary versions. There might be some updates after the lectures.
  
  
• February 9th, 2005.
  
  • Errata list for "A Note on Game Characterization of Strong and Weak Bisimilarity" and "An Intro to Milner's CCS" has been updated.
  • Solutions to exercise set 2 are on-line. The slides from the lectures are now available also in print-friendly version.
  • There is a research talk today given by A. Møller from Aarhus University. The topic is a verification of programs with pointers. More information can be found here. Students interested in the topic are welcome to attend the talk.
  
  
• February 7th, 2005.
  Solutions to exercise set 1 and slides from lecture 2 are now on-line (in lectures plan).
  
  
• February 4th, 2005.
  
  • Compendiums are now again available at the bookstore. This time there is only one containing both parts (it has white cover). The price is the same as before.
  • The group division for the tutorials is available here.
  
  
• February 2nd, 2005.
  Slides from the first lecture and the tutorial exercises for Monday are now on-line in the lectures plan.
  
  
• February 1st, 2005.
  The compendiums were sold out very fast today. We have ordered extra pieces and they should be available on Friday or Monday (latest).
  
  
• January 30th, 2005.
  Lectures plan is updated.