Symbolic profiling and repair

Many tools rely on symbolic evaluation to reduce programming tasks, such as verification and synthesis, to satisfiability queries. Using a symbolic evaluator effectively requires tool developers to be able to identify and repair performance bottlenecks in code under all-path evaluation, a difficult task, even for experts. SymPro and SymFix are systems that automate this task.

SymPro implements symbolic profiling, a new approach to identifying performance bottlenecks in programs under symbolic evaluation. SymPro identifies bottlenecks by analyzing two implicit resources at the core of every symbolic evaluation engine, the symbolic heap and symbolic evaluation graph. These resources form a general performance model of symbolic evaluation.

SymFix implements a new method for repairing bottlenecks found by SymPro. The key idea is to formulate the symbolic performance repair problem as combinatorial search through a space of semantics-preserving transformations, or repairs, to find an equivalent program with minimal cost under symbolic evaluation. SymFix uses symbolic profiling to guide the search for repairs.


SymPro is integrated into the Rosette solver-aided language and the Crucible symbolic evaluation engine developed by Galois. It has been used to develop the Serval verification framework, and find and repair performance bottlenecks in many existing Rosette-based tools.



The Rosette Guide: Performance


SymPro is integrated into Rosette at The artifact for the OOPSLA 2018 paper is available here.

SymFix is available at