Harnessing Forest Automata for Verification of Heap Manipulating Programs

This work addresses verification of infinite-state systems, more 
specifically, verification of programs manipulating complex dynamic 
linked data structures. Many different approaches emerged to date, but 
none of them provides a~sufficiently robust solution which would succeed 
in all possible scenarios appearing in practice. Therefore, in this 
work, we propose a new approach which aims at improving the current 
state of the art in several dimensions. Our approach is based on using 
tree automata, but it is also partially inspired by some ideas taken 
from the methods based on separation logic. Apart from that, we also 
present multiple advancements within the implementation of various tree 
automata operations, crucial for our verification method to succeed in 
practice. Namely, we provide an optimised algorithm for computing 
simulations over labelled transition systems which then translates into 
more efficient computation of simulations over tree automata. We also 
give a new algorithm for checking inclusion over tree automata, and we 
provide experimental evaluation demonstrating that the new algorithm 
outperforms other existing approaches.