Profile-Guided Constraint Simplification for Symbolic Execution
This program is tentative and subject to change.
Constraint solving remains the primary bottleneck in symbolic execution, consuming up to 90% of analysis time. We present EVP (Empirical Value Profiling), a framework that leverages runtime profiling to optimize constraint solving within LLVM-based symbolic execution engines. EVP identifies program variables that consistently assume limited sets of concrete values during execution, then provides this information through a standardized API that symbolic executors can use to simplify constraints. Our framework consists of three decoupled components: (1) an LLVM-based profiler that tracks variable values at branch points, (2) a value analyzer that identifies limited-domain variables using configurable thresholds, and (3) a constraint simplification API that integrates with any SMT-based symbolic executor. We demonstrate EVP’s generalizability by integrating it with KLEE achieving 12.4-85.2% reduction in constraint-solving time across the benchmark programs while maintaining minimal trade-off. EVP’s modular design enables adoption by existing tools without major architectural changes, establishing empirical profiling as a practical optimization for symbolic execution.
This program is tentative and subject to change.
Mon 13 AprDisplayed time zone: Brasilia, Distrito Federal, Brazil change
14:00 - 15:30 | Session 5: Automated Reasoning, and Program AnalysisResearch Track / FormaliSE Program at Oceania VIII | ||
14:00 30mTalk | Profile-Guided Constraint Simplification for Symbolic Execution Research Track Roxana Shajarian University of Nebraska-Lincoln, Md Rashedul Hasan University of Nebraska-Lincoln, Lisong Xu University of Nebraska-Lincoln, USA, Hamid Bagheri University of Nebraska-Lincoln | ||
14:30 15mTalk | BPMN-T: A Timed–Probabilistic Extension of BPMN with Formal Semantics Research Track Ahang Zuo Univ. de Pau et des Pays de l’Adour | ||
14:45 15mTalk | Toward an automatic formal verification of Cairo v0 programs (Extended Abstract) Research Track | ||