Acknowledgements

Spatial Logics are used to reason about data structures and hierarchical net-work structures. Automated decision procedures for these logics allow us to formally verify the properties of a system, highlighting errors in the system be-fore it is released. A specic instance of Spatial Logics is the Tree Logic, which describes the structural properties of semi-structured data, such as XML. Previ-ous decision procedures for this logic suered a complexity bound by a tower of exponentials, meaning that an implementation of the procedure did not run in viable times. Recently, Dal Zilio et al have proposed a new decision procedure for the Tree Logic, with a complexity that is doubly exponential. We provide the rst implementation of this approach, and discover, through the use of several optimisations, that the decision procedure is viable. Furthermore, we take this decision procedure as an inspiration and produce two new decision procedures for the Separation Logic | a logic for reasoning about memory heap structures with a stack and pointers. The rst decision procedure involves a translation from the Separation Logic to the Tree Logic, whilst the second procedure shows that the Separation Logic can be expressed in First-Order Logic with Equality