XML Static Analyzer User Manual

This paper describes the logical solver introduced in Geneves, 2006; Geneves et al., 2007 and provides informal documentation for using its implementation. The solver allows automated verification of properties that are expressed as logical formulas over trees. A logical formula may for instance express structural constraints or navigation properties (like e.g. path existence and node selection) in finite trees. A decision procedure for a logic traditionally defines a partition of the set of logical formulas: formulas which are satisfiable (there is a tree which satisfies the formula) and remaining formulas which are unsatisfiable (no tree satisfies the given formula).