Architecture for a Symbolic Execution Environment

Program testing is an important aspect of software development. Symbolic execution can be used as a tool to automatically verify the correctness of programs for all feasible paths of execution. Moreover, for embedded systems symbolic execution can be used to generate test cases to estimate run times to help determine the worst-case execution time (WCET) and schedulability of systems. This thesis explores an architecture for symbolic execution for use in embedded Rust. Accompanied with the architecture are implementation details of a prototype Symex that can handle small programs. Symex evaluates all feasible paths of execution looking for errors and assertions, and reports which concrete inputs lead to errors. Included with the prototype is a command-line tool to automatically build and analyze Rust projects. The tool allows for easy analysis of projects, and an included library provides functions to manipulate symbolic variables to aid the analysis. The method of evaluating all feasible paths work well with the purpose of evaluating embedded systems, where the aim is typically to keep the code complexity low. The low code complexity lends the software to be resilient towards path explosion. For the cases where this cannot be helped the functions to manipulate the symbolic variables in the analysis can be used to further constrain the variables and lower the number of feasible paths. The evaluation shows the architecture is feasible for the intended use case in embedded systems. Furthermore, evaluation of the prototype shows how the system can be used to show the absence of errors, verify functions, and check for functional equivalence. Inherent to the symbolic execution approach the system cannot handle programs with a large branching factor