Model Checking with System Call Traces

When executing programs, DIVINE can record system call invoked by the tested program in the form of a trace. This trace can be subsequently used during model checking to replay these system calls back to the program. However, only executions that exactly correspond to the system call trace can be explored by DIVINE. In this thesis, I introduce improvements to the coverage of a program verified by DIVINE with the usage of the recorded system call traces. The first improvement is based on defining and implementing weaker condition which allows a commutation of system calls in the captured trace. This improves the original linear order of the trace to a partial order. The second improvement is based on the introduction of non-deterministic mutations into the traces which can deviate program to different paths of execution, which are possibly filled with errors. Additionally, I also discuss various techniques for modifying traces to achieve the best possible result.