Automatic verification of temporal and timed properties of control programs. - Bohumir Zoubek (2004)