I'm following a course called "Concurrent and Distributed Programming" (CDP). It concerns programs that run at the same time in a multiprocessor, multiprogrammed or multiple device environment. The main part of the course is proving correctness of such programs. In layman's language: If multiple things happen at once (such as lots of cars driving on a crossing), how do you prevent certain things from happening together (cars driving in perpendicular directions) without the risk of waiting forever (always letting one direction first).

Pretty interesting stuff, actually. Quite a different mindset from normal programming. I've already had some experience with this in other courses (Operating Systems, Programming), but this is more formal and actually proves that algorithms are correct. Something I like :-)

The nasty side of it is that the classes are pretty chaotic. The teacher doesn't really do a good job at explaining the stuff. Add to that that a lot of her sheets (containing very formal, non-trivial to understand code) contain stupid errors and you get a pretty lousy class.

Anyway, I've been installing spin, the validation tool used for this course. I have yet to understand what it can do, though. For now, I was able to do the first (easy) assignment by clicking around in the graphical front-end, xspin. Both are pretty easy to install. Spin is written in C and needs a simple compilation, xspin is TCL/TK and works out right away (if you follow instructions).

The bigger challenge was to make a screenshot of the application showing the simple Promela model, the output and my name. After doing the necessary resizing and converting (I had to hand in the screenshot in PDF format...), I got it done. Let's hope the classes will improve a little and this might turn out to be a fine course.