A device configured to provide a software verification tool that enables source code to be split into a plurality of modules, each module including a portion of the source code, the device comprising: one or more processors to: create a graph based on source code, the graph including representations of variables and functions provided in the source code, the representations being nodes of the graph, each of the nodes representing one of the variables or one of the functions, the nodes being connected to represent dependencies among the nodes, analyze the source code to identify private variables and functions of the source code and public variables and functions of the source code, wherein the private variables and functions may only be used inside each module, and wherein the public variables and functions may be used outside of each module, determine, based on the graph, a maximum size threshold for each module of the plurality of modules, the maximum size threshold including a number of lines of the source code, a number of public and/or private functions or a number of public and/or private variables, assign, based on the graph, the private variables and functions to a corresponding module of the plurality of modules, reduce, based on the graph, a number of the public variables and functions assigned to each module by: determining relations of the public variables and functions with other modules; and selecting, for each module, the public variables and functions that have a number of relations with other modules that is less than a threshold value; generate the plurality of modules based on the graph and the assigned private variables and functions, and one or more of the maximum size threshold and the number of the public variables and functions assigned to each module, by: giving each variable and/or function, provided in a node, a value that depends on a physical size associated with the variable or function, respectively; combining two or more nodes of the graph together to create each module; for each module, ensuring that a complexity of the module does not exceed a maximum value; and use the plurality of modules to perform verification of the source code, where, when using the plurality of modules to perform the verification of the source code, the one or more processors are further to one of: verify the plurality of modules, in serial, to perform the verification of the source code, or verify the plurality of modules, in parallel, to perform the verification of the source code. create a graph based on source code, the graph including representations of variables and functions provided in the source code, the representations being nodes of the graph, each of the nodes representing one of the variables or one of the functions, the nodes being connected to represent dependencies among the nodes, analyze the source code to identify private variables and functions of the source code and public variables and functions of the source code, wherein the private variables and functions may only be used inside each module, and wherein the public variables and functions may be used outside of each module, determine, based on the graph, a maximum size threshold for each module of the plurality of modules, the maximum size threshold including a number of lines of the source code, a number of public and/or private functions or a number of public and/or private variables, assign, based on the graph, the private variables and functions to a corresponding module of the plurality of modules, reduce, based on the graph, a number of the public variables and functions assigned to each module by: determining relations of the public variables and functions with other modules; and selecting, for each module, the public variables and functions that have a number of relations with other modules that is less than a threshold value; determining relations of the public variables and functions with other modules; and selecting, for each module, the public variables and functions that have a number of relations with other modules that is less than a threshold value; generate the plurality of modules based on the graph and the assigned private variables and functions, and one or more of the maximum size threshold and the number of the public variables and functions assigned to each module, by: giving each variable and/or function, provided in a node, a value that depends on a physical size associated with the variable or function, respectively; combining two or more nodes of the graph together to create each module; for each module, ensuring that a complexity of the module does not exceed a maximum value; and giving each variable and/or function, provided in a node, a value that depends on a physical size associated with the variable or function, respectively; combining two or more nodes of the graph together to create each module; for each module, ensuring that a complexity of the module does not exceed a maximum value; and use the plurality of modules to perform verification of the source code, where, when using the plurality of modules to perform the verification of the source code, the one or more processors are further to one of: verify the plurality of modules, in serial, to perform the verification of the source code, or verify the plurality of modules, in parallel, to perform the verification of the source code. verify the plurality of modules, in serial, to perform the verification of the source code, or verify the plurality of modules, in parallel, to perform the verification of the source code.