Formale Verifikation auf höheren Entwurfsebenen mittels symbolischer Traversierung unendlicher Automaten.