Szimbolikus modellellenőrzés és végrehajtási szekvencia generálás vezérelt kereséssel