The construction of a T-system formal model and the proof of its correctness

We study the methods of program parallelization used in the T-system (an automatic parallelization tool for applied programs). A distinguishing feature of the T-system is that it is designed for programs written in the widespread languages C and C++. In this paper we present a formal model describing the T-system basic constructions on the basis of operational approach. Our model is used to prove the correctness of T-system mechanisms.