Fares Fraij, 12/3/03 A Framework for Verifying HATS Abstract: The High-Assurance Transformation system (HATS) is a language independent program transformation system whose goal is to provide a transformation-oriented programming environment facilitating the development of transformation rules and strategies whose correctness can be formally verified. In HATS, programs are defined by a context-free grammar. These programs are manipulated internally as Syntax Derivation Trees (SDT). HATS manipulate the SDTs by transformation rules and strategies, which are defined using a special purpose language. The output is also an SDT that results from applying the transformation rules (TR) to the input SDT according to a control strategy. The goal of our work is to prove that the application of these transformation rules and strategies preserves semantics. Our modeling and verification framework of the transformation system (HATS) is similar to the framework that was adapted in verifying parts of the implementations of the JVM. Our model consists of a state and a state transition function. The state consists an SDT, a control operator, a transformation sequence, and two Program counters (PCs), one to keep track of the next transformation rule (TR) to be applied and the other to keep track of the next node to apply the TR to, respectively. The transition function is the function that takes the current state and returns a new state that results from applying the current TR. We start with the control operator "once" that applies the transformation sequence one time per node and traverses the SDT one time. We are trying to apply "once" in a top-down fashion. Thereafter, we can go on and model some other control operators that were added in the recent version of HATS. For the verification part, we will use simple arithmetic expressions since we can obtain semantics function for such expressions. The verification effort will be to show that the TR preserves the meaning