FormaliSE 2026
Sun 12 - Mon 13 April 2026 Rio de Janeiro, Brazil
co-located with ICSE 2026

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 Apr

Displayed 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
30m
Talk
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
15m
Talk
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
15m
Talk
Toward an automatic formal verification of Cairo v0 programs (Extended Abstract)
Research Track