ABSTRACT
In the early 1980s an alternative to using proof rules was proposed, independently by researchers in Europe [53] and the US [19], that given a (finite) model of a program systematically checks whether it satisfies a given property. This breakthrough was the first step towards the automated verification of concurrent programs. Typical questions treated by “model checking” are:
• safety: e.g., does a given mutual exclusion algorithm guarantee exclusive access to the shared resource?
