Forester: Shape Analysis Using Tree Automata

Forester is a tool for shape analysis of programs with complex dynamic data structures--including various flavours of lists such as singly/doubly linked lists, nested lists, or skip lists as well as trees and other complex data structures--that uses an abstract domain based on finite tree automata. This paper gives a brief description of the verification approach of Forester and discusses its strong and weak points revealed during its participation in SV-COMP'15.