Two ASSET exercises have been added to the Exercises document. For 2016-09-16, please solve exercise 17 as far as you can. We will discuss your incomplete solutions. Then, for 2016-09-20, complete the solution of exercise 17.
A link to the MathCheck parser manuscript has been added to the right.
Two links to MathCheck exercises have been added to the right.
The course starts on Tuesday, 2016-08-30 at 12:15, in classroom TD 308.
Model checking means the use of automated mathematical methods for checking a design of a software or hardware system against errors. Model checking has been successfully used to find bugs that are too rare to be found in testing, but frequent enough to be dangerous. This course covers the general issues in model checking, introduces the most important approaches to model checking, and discusses some techniques in detail.
Petri nets are a mathematical formalism for representing concurrent systems, that is, systems that consist of co-operating components: program threads, hardware units, a mobile phone and the network, …. Thanks to their intuitive graphical representation, Petri nets are well-suited to studying concurrency. Being computationally strictly between finite automata and general computers, they offer interesting algorithmical advantages (at the cost of modelling disadvantages). This course focuses on those aspects of Petri nets that are relevant for model checking.
Pedagocically, the goal of the course is less in the listed topics themselves, and more in learning how theoretical computer science can be used to solve practical problems. The timing of the course is flexible. If necessary, some time will be devoted to background topics in algorithms, theoretical computer science, and logic, to help students with moderate background.
On the other hand, the most advanced topics in the course are directly linked to international top-level research. For instance, we won the 2014 Computer-Aided Verification award and 2012 Petri net outsanding paper award. So this course has something to offer also to ambitious students.
The course is intended for both finnish and international students interested in advanced programming issues, theoretical computer science, or discrete mathematics.
If you know how graphs are represented in programs and how depth-first search works, then your background in programming is probably sufficient. Basic notation from set theory and especially logic suffices for background in mathematics. No background in theoretical computer science is assumed.
That is, you need not know much theory now to take the course. However, please be aware that you must learn the theory taught during the course to pass the course. If your plan is to concentrate on the practical side of the course and skip the theory taught in the course, then this course is not for you.
Attitude is more important than background. If your background is weaker than mentioned above, but you are ready to solve extra personal exercises designed for you, then you are welcome to the course. The deal is: I will do my best to adapt the course to your background, and you will do your best to learn during the course.
The course is on periods 1 and 2. Every week there are three meetings of two hours each. The meetings are flexibly used for lectures, exercises, and discussion. The meetings are on
An assignmnent consists of one or more exercises. You are expected to solve them at home and present the solutions in a meeting. In addition to traditional mathematical, programming, or algorithm design tasks, an exercise may also ask you to find information on some topic and prepare a talk on it. There will also be hands-on model checking exercises using a simple model checker called ASSET.
I plan to design personal assignments adapted to your background and performance. A typical assignment consists of one medium-sized or big exercise, or many small exercises. If an assignment is exceptionally big, then some other assignment to the same student will be exceptionally small, to balance the average workload.
There will be two alternative ways to do the course.
The recommended way is to do 28 assignments. You must present a solution to an assignment in at least two thirds of the meetings, and there must not be more than four meetings in a row without you presenting a solution. (If, for some strong reason, this is or becomes impossible, then please contact me as soon as possible.) I will collect information on your performance during the course, and give a mark based on that.
The alternative way is to solve 10 assignments and then take the examination. The assignments that you solve during the course are counted in those 10, and the rest you can do on your own and send their solutions to me. Please contact me to get the missing assignments early enough, so that you can solve them and I can browse the solutions before the deadline for registering to the examination. The mark is based on the examination only. The purpose of the assignments is to ensure that students do not try the examination without studying anything.
Information on reading material will be provided later. All material will be distributed via this web page or emailed to you.
The teacher of the course is Antti Valmari.
This list of topics is initial and may change.