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čitouformu kvantitaivních omezení nad velikostí přijímaných stromů a jejichpodstromů. Je ukázáno, že navržená třída má celou řadu  žádoucíchjazykově-teoretických vlastností (uzavřenost, rozhodnutelnost). Tatotřída je motivována využitím v automatizované verifikaci programůmanipulujících vyvážené stromové struktury (Red-Black trees, AVLtrees). Je ukázáno, že operace používané pro manipulaci takovýchstruktur lze realizovat nad vhodně zvolenou podtřídou navrženýchstromových automatů. To tvoří základ pro semi-automatickou metoduformá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).