1. What?

2. To Whom?

3. Implementation

4. Contents

Points

Exercises

Reading material

The ASSET model checker

MathCheck minicourse
on writing predicates

Other MathCheck
exercises

MathCheck parser
manuscript

MAT-74506 In Curriculum Book

TCS Studies

Computer-Aided
Verification Award 2014

Updated 2016-11-16

Some exercises have been added to the Exercises document. Some links to block splitting algorithms have been added to the List of reading material.

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

**Tuesdays 12:15–14 in TD 308**(except 2016-12-06),**Thursdays 10:15–12 in TB 206**, and**Fridays 10:15–12 in TC 163**.

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*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.**28 assignments**.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.

- Petri nets
- informal introduction via graphical representation
- definition of place/transition nets
- enabled transitions and firing of transitions
- other classes of Petri nets

- Behaviour of Petri nets
- reachability set and reachability graph
- boundedness
- some liveness concepts
- strong components of the reachability graph

- Checking simple properties from the reachability graph
- deadlocks and termination
- bad states
- non-progress cycles
- Büchi acceptance

- State explosion
- the problem
- on-the-fly verification
- bit-state hashing
- exploiting symmetry
- exploiting parallel hardware

- A quick look on invariants and structure theory
- place invariants
- transition invariants
- traps and siphons
- free-choice nets

- Temporal logics
- Linear-time Temporal Logic
- safety, liveness and fairness
- Computation Tree Logic (branching time)
- Computation Tree Logic Star

- Model-checking temporal logics
- basic CTL verification algorithm
- translation of LTL to Büchi automata
- computational complexity

- Stubborn sets (partial-order verification)
- deadlock-preserving method
- construction of stubborn sets
- verifying safety properties
- verifying linear-time properties
- verifying branching-time properties

- Binary decision diagrams
- definition
- verification algorithms
- complexity considerations

- Bounded model checking
- SAT solvers
- translation to SAT
- more general solvers

- Coverability sets
- mathematics
- modern algorithm

- Conclusion