In the CoLiS project (for Correctness of Linux Scripts), our mid-term goal is to automatically verify certain properties on installation packages that may include shell scripts. In order to do that, we want to write a symbolic execution tool that would compute abstract specification for each installation script in term of filesystem transformations.

We investigate a logic of an algebra of trees with an update operation, which expresses that a tree is obtained from an input tree by replacing a particular direct subtree while leaving the rest intact. This operation improves on the expressivity of existing logics of tree algebras in our case of feature trees. These allow for an unbounded number of children of a node in a tree.

We show an efficient way of testing the satisfiability of existential clauses in this algebra that can lead to an efficient implementation of our symbolic execution engine. We also show the decidability of the first-order theory of this algebra via a weak quantifier elimination procedure which is allowed to swap existential quantifiers for universal quantifiers.