An important issue in the development of large software systems is the specification of its desired structural and dynamic properties. To avoid the impreciseness and ambiguities of specifications in natural language, a number of specialized formal languages, based on mathematics, have been developed: Hoare logic, Petri Nets, Process calculi, etc. Moreover, these languages are supported by tools allowing various types of analysis and verification. The SPIN system is a prominent example of that.
The course starts with an introduction into Hoare logic, an approach that has had a major impact on the development of the area.
Then a few sessions are devoted to the study of a verification problem (reachability) and it is demonstrated how a mathematical analysis of this problem leads to a flexible verification algorithm. In the last part of the course the SPIN/PROMELA verification system and its mathematical background are discussed.