Tomáš Fiedor: Formální analýza a verifikace konečnosti běhu a spotřeby zdrojů programy

Dokazování konečnosti běhu a spotřeby zdrojů programů manipulujících se složitými dynamickými strukturami je jednou z méně zkoumaných oblastí formální analýzy a verifikace. V prezentaci stručně představím (i) stávající metody a vlastní navrhovaný počáteční přístup založený na stromových automatech a současně (ii) paralelně probíhající výzkum v oblasti rozhodovaní logiky WSkS. Stručně představím své dosavadní výsledky a budoucí cíle.