Critical Infrastructure Systems (CIS) need to be more reliable. CIS are present in most life aspects, including hospitals, factories, aviation, and governmental venues. With the surge of interest on the Internet of Things (IOT), the number of devices in use will likely continue increasing for years to come. However, since any of these systems contained essentially software or hardware, all of them can pose reliability risks as well. Finding software bugs in CIS depends on analyzing machine code, as the software is generally proprietary. Due to software complexity, manual testing is not enough to guarantee the correct behavior of software. One alternative to this limitation is known as Symbolic Execution (SE). SE is a formal verification method that simulates software execution using symbolic values instead of concrete ones. The execution starts with all input variables unconstrained, and assignments that use any input variable are encoded as logical expressions. Whenever a branch is reached, the SE engine checks which values the branch condition can assume. If more than one valid evaluation is possible, the execution forks, and a new process is created for each possibility. This thesis will apply the concept of SE on software systems and show its efficiency to find software bugs at the early stage of software development life cycle. Furthermore, it shows how this can be applied to improve certification process of software systems. This thesis uses the state-of-the-art SE tool KLEE [78] in order to assess the proposed technique.