At the end of the course, each participant

• is able to identify (aspects of) problems that can be solved with Spin (and problems that cannot);
• is able to model reasonably complex systems in Promela with a good sense of economy as far as memory and time demands are concerned;
• is able to phrase correctness claims in terms of Linear Temporal Logic or Promela never claims ;
• is able to efficiently use the validator to check correctness with the for Spin highest possible coverage
• has an understanding of the underlying theory, sufficient to judge the values of model checking in comparison to simulation and to keep up with developments in the field;
• ... and has enjoyed the course.