Abstract:
Spin is a model checker that is widely used for verification of concurrent and distributed systems. The talk will present techniques and tools for teaching concurrency and nondeterminism using Spin. Spin can replace concurrency simulators and can also generate scenarios that demonstrate errors like race conditions and starvation. The implementation of nondeterministic algorithms and finite automata in Spin will be described, together with the use of search diversity to demonstrate random algorithms and parallelism. The tools to be presented are: jSpin, a development environment for Spin; VMC, a tool that generates a diagram of the state space of a model; VN for visualizing nondeterminism; Erigone, a reimplementation of Spin designed for pedagogical use.

Short-Bio:
Mordechai (Moti) Ben-Ari is a full professor in the Department of Science Teaching of the Weizmann Institute of Science, where he heads the computer science education group. He is the author of numerous textbooks, including Principles of Concurrent and Distributed Computation, and Mathematical Logic for Computer Science. His group, in collaboration with the University of Eastern Finland, developed the Jeliot program animation system. In 2004, he received the ACM/SIGCSE Award for Outstanding Contributions to Computer Science Education, and in 2009 he was elected as a Distinguished Educator of the ACM.