Symbolic analysis of complex software systems
Generation of concurrent test cases (inputs, interleavings and oracles) for shared memory, message passing and event driven system.
Latest Results:
- Symbolic execution of complex heap data structures (ISSTA 2017) and reuse of constraint proofs (ICSE 2017).