[Pl-seminar] Friday - Guannan Wei: Compiling and Controlling Symbolic Execution

[Luna Phipps-Costin]

Hello all -
I am pleased to inform you all that on December 1st, Guannan Wei will be speaking at our seminar.   Looking forward to seeing you there.

Speaker: Guannan Wei
Title: Compiling and Controlling Symbolic Execution
Abstract:
Symbolic execution is a powerful program analysis and testing technique. Symbolic execution engines are usually implemented as interpreters, and the induced interpretation overhead can dramatically inhibit performance. Alternatively, implementation choices based on instrumentation provide a limited ability to transform programs. However, the use of compilation and code generation techniques beyond simple instrumentation remains underexplored for engine construction, leaving potential performance gains untapped.

In this talk, I will talk about how to improve the performance of symbolic execution via sophisticated compilation techniques. The key insight is to compile nondeterministic symbolic execution semantics into cooperative concurrency via continuation-passing style, which completely eliminates interpretation overhead and effectively controls multiple paths in the compiled form of symbolic execution. This compilation schema further leads to efficient parallel symbolic execution. I will also present GenSym, the symbolic-execution compiler we build for LLVM’s IR based on multi-stage programming and compilation with continuation-passing style. We evaluate the performance of GenSym, and show significant speedups on several real-world Coreutils programs compared with the state-of-the-art symbolic interpreter KLEE.
When: Friday, December 1st. Lunch from 12 to 12:30, talk from 12:30 to 1:30
Where: Forsyth 237
Bio: Guannan Wei is a postdoc at Purdue University working in static analysis, compilers, and type systems. He obtained his PhD in 2023 from Purdue University under the supervision of Tiark Rompf.
-------------- next part --------------
HTML attachment scrubbed and removed