Translating flowcharts to non-deterministic languages

Modeling languages are used to verify software and can be classified into deterministic modeling languages and non-deterministic modeling languages. Deterministic modeling languages have a single thread of control whereas non-deterministic ones have a multitude of threads of control and are more amenable for program transformations and analyses. However, deterministic languages such as control-flow graphs are pre-dominantly used in programming language tools. In this work, we translate programs in a deterministic flowchart language to a non-deterministic algebraic modelling language. For the translation, we employ the technique of converting a finite state automata to a regular expression. The states of the finite state automata represent states in the control-flow graph, and the edges represent the edges in the control-flowgraph.We construct a homomorphism to show that the translation is sound, i.e., we prove that the semantics of the program in the deterministic flowchart language is preserved in the translation. Experiments on our implemented algorithm are conducted on the SPEC benchmark suite