The application of hypergroups in symbolic executions and finite automata

Symbolic execution is one of the most important testing techniques to ensure the quality of software systems that need to be dependable and reliable. This technique systematically explores the program of the subject system which is represented by an Inter-procedural Control Flow Graph (ICFG). An ICFG is a graph that combines Control Flow Graphs (CFGs) of the program procedures by connecting each CFG with its call nodes. The existence of unreachable CFGs and infinite loops increases the complexity and runtime of a program, while they have no effect on testing the program. In this paper, we present an approach to convert the ICFG of a program to the corresponding finite automaton, called ICFG-automaton. Then, we construct a quasi-ordering hypergroup on the set of states of the ICFG-automaton and prove that the inner irreducibility in hypergroups is equivalent to the connectivity in CFGs. Moreover, we show that if every sub-automaton of an ICFG-automaton is a sub-hypergroup, then the program has an infinite loop. These results identify the parts of a program that should be modified to decrease the complexity of the testing activity.