SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Thu 19 Nov 2020 11:00 - 11:20 at SPLASH-I - R-3 Chair(s): Marieke Huisman, Michael Coblenz
Thu 19 Nov 2020 23:00 - 23:20 at SPLASH-I - R-3 Chair(s): Pranav Kant, Xiangzhe Xu

Building effective symbolic execution engines poses challenges in multiple dimensions: an engine must correctly model the program semantics, provide flexibility in symbolic execution strategies, and execute them efficiently.

This paper proposes a principled approach to building correct, flexible, and efficient symbolic execution engines, directly rooted in the semantics of the underlying language in terms of a high-level definitional interpreter. The definitional interpreter induces algebraic effects to abstract over semantic variants of symbolic execution, e.g., collecting path conditions as a state effect and path exploration as a nondeterminism effect. Different handlers of these effects give rise to different symbolic execution strategies, making execution strategies orthogonal to the symbolic execution semantics, thus improving flexibility. Furthermore, by annotating the symbolic definitional interpreter with binding-times and specializing it to the input program via the first Futamura projection, we obtain a "symbolic compiler", generating efficient instrumented code having the symbolic execution semantics. Our work reconciles the interpretation- and instrumentation-based approaches to building symbolic execution engines in a uniform framework.

We illustrate our approach on a simple imperative language step-by-step and then scale up to a significant subset of LLVM IR. We also show effect handlers for common path selection strategies. Evaluating our prototype's performance shows speedups of 10~30x over the unstaged counterpart, and ~2x over KLEE, a state-of-the-art symbolic interpreter for LLVM IR.

Thu 19 Nov
Times are displayed in time zone: Central Time (US & Canada) change

11:00 - 12:20: R-3OOPSLA at SPLASH-I +12h
Chair(s): Marieke HuismanUniversity of Twente, Michael CoblenzUniversity of Maryland at College Park
11:00 - 11:20
Talk
OOPSLA
Guannan WeiPurdue University, Oliver BračevacPurdue University, Shangyin TanPurdue University, Tiark RompfPurdue University
Link to publication DOI Pre-print Media Attached
11:20 - 11:40
Talk
OOPSLA
Gushu LiUniversity of California at Santa Barbara, Li ZhouMax Planck Institute for Security and Privacy, Nengkun YuUniversity of Technology Sydney, Yufei DingUniversity of California at Santa Barbara, Mingsheng YingUniversity of Technology Sydney / Institute of Software at Chinese Academy of Sciences / Tsinghua University, Yuan XieUniversity of California at Santa Barbara
Link to publication DOI Pre-print Media Attached
11:40 - 12:00
Talk
OOPSLA
Hamed GorjiaraUniversity of California at Irvine, Guoqing Harry XuUniversity of California at Los Angeles, Brian DemskyUniversity of California at Irvine
Link to publication DOI Media Attached
12:00 - 12:20
Talk
OOPSLA
Cormac FlanaganUniversity of California at Santa Cruz, Stephen N. FreundWilliams College
Link to publication DOI Media Attached
23:00 - 00:20: R-3OOPSLA at SPLASH-I
Chair(s): Pranav KantUniversity of Utah, Xiangzhe XuNanjing University
23:00 - 23:20
Talk
OOPSLA
Guannan WeiPurdue University, Oliver BračevacPurdue University, Shangyin TanPurdue University, Tiark RompfPurdue University
Link to publication DOI Pre-print Media Attached
23:20 - 23:40
Talk
OOPSLA
Gushu LiUniversity of California at Santa Barbara, Li ZhouMax Planck Institute for Security and Privacy, Nengkun YuUniversity of Technology Sydney, Yufei DingUniversity of California at Santa Barbara, Mingsheng YingUniversity of Technology Sydney / Institute of Software at Chinese Academy of Sciences / Tsinghua University, Yuan XieUniversity of California at Santa Barbara
Link to publication DOI Pre-print Media Attached
23:40 - 00:00
Talk
OOPSLA
Hamed GorjiaraUniversity of California at Irvine, Guoqing Harry XuUniversity of California at Los Angeles, Brian DemskyUniversity of California at Irvine
Link to publication DOI Media Attached
00:00 - 00:20
Talk
OOPSLA
Cormac FlanaganUniversity of California at Santa Cruz, Stephen N. FreundWilliams College
Link to publication DOI Media Attached