Symbolic execution is a technique to analyze a program depending on sets of input values by means of a symbolic interpreter. It can be used to generate test cases for software testing, but also to generate verification conditions in program logics to prove program correctness. This thesis will study how program verification and program testing can be combined, based on symbolic execution.
Suggested coursework
- IN5170 - Models of concurrency.
- IN5100 - Selected topics in rewriting logic.
- IN5110 - Specification and verification of parallel systems.