Automata-based Verification of Programs with Tree Updates

formální verifikace, symbolické metody, teorie automatů, stromové utomaty, automaty s kvantitativními omezeními

Článek zavádí novou třídu stromových automatů rozšířených o určitou formu kvantitaivních omezení nad velikostí přijímaných stromů a jejich podstromů. Je ukázáno, že navržená třída má celou řadu  žádoucích jazykově-teoretických vlastností (uzavřenost, rozhodnutelnost). Tato třída je motivována využitím v automatizované verifikaci programů manipulujících vyvážené stromové struktury (Red-Black trees, AVL trees). Je ukázáno, že operace používané pro manipulaci takových struktur lze realizovat nad vhodně zvolenou podtřídou navržených stromových automatů. To tvoří základ pro semi-automatickou metodu formální verifikace programů manipulujících zmíněné datové struktur, jež se velmi často používají v kritických programových dílech(operační a řídicí systémy).