Under the hood: XACT analysis

Our idea:

• Use static analysis to validate XACT transformations

Given an XACT transformation and a DTD schema, the possible answers are:

• "The output is always valid with respect to the schema"
• "The output might be invalid with respect to the schema, but I am not sure"

The main challenges are:

• Extract the XACT control-flow from the Java program
• Define a suitable abstraction of XML template values
• Define data-flow equations modelling the XACT operations

This analysis heavily exploits the immutability!