Symbolic execution is a technique to analyze a program depending on sets of input values by means of a symbolic interpreter. In contrast, program logics such as Hoare logic analyze a program backwards to derive the weakest precondition (i.e., the largest set of input values to reach a given final state). It is interesting to understand how symbolic execution will work in a backwards setting. This project consists of developing a symbolic interpreter for backwards symbolic execution of a small parallel programming language.
Suggested coursework
- IN5170 - Models of concurrency
- IN5100 - Selected topics in rewriting logic
- IN5110 - Specification and verification of parallel systems
Reference
Frank S. de Boer, Einar Broch Johnsen, Rudolf Schlatte, Silvia Lizeth Tapia Tarifa, Lars Tveito: Inseguendo Fagiani Selvatici: Partial Order Reduction for Guarded Command Languages. Gabbrielli's Festschrift 2020: 10:1-10:18 [Link]