AG 1, AG 2, AG 3, AG 4   Info

AG Audience

60 Minutes

Saarbrücken

This talk presents a novel model-checking procedure for first-order CTL. The procedure relies on a partition of the system variables into control and data. While control values are expanded into BDD-representations as it is done in ordinary (symbolic) model checking, data values enter in form of their properties relevant to the verification task. The algorithm is completeley automatic. If it terminates , it has generated a fist-order verification condition on the data space which characterizes the system's correctness. Termination can be guaranteed for a class that for instance properly includes the data-independent systems studied by Wolper, and many common types of embedded controllers. The algorithm has been implemented and successfully applied to industrial case studies.

Tom Henzinger

301

--email hidden

passcode not visible

logged in users only