Speeding up SMT Solving via Compiler Optimization

Dec 6, 2023

Speakers

About

SMT solvers are fundamental tools for reasoning about constraints in practical problems like symbolic execution and program synthesis. Faster SMT solving can improve the performance and precision of those analysis tools. Existing approaches typically speed up SMT solving by developing new heuristics inside particular solvers, which requires nontrivial engineering efforts. This paper presents a new perspective on speeding up SMT solving. We propose SMT-LLVM Optimizing Translation (SLOT), a solver-agnostic pre-processing approach that utilizes existing compiler optimizations to simplify SMT problem instances. We implement SLOT for the two most application-critical SMT theories, bitvectors and floating-point numbers. Our extensive evaluation based on the standard SMT-LIB benchmarks shows that SLOT can substantially increase the number of solvable SMT formulas given fixed timeouts. Moreover, it achieves average $1.5\times$ speedups for bitvector benchmarks and almost $5\times$ speedups for large floating-point benchmarks.

Organizer

Categories

Store presentation

Should this presentation be stored for 1000 years?

How do we store presentations

Total of 0 viewers voted for saving the presentation to eternal vault which is 0.0%

Sharing

Recommended Videos

Presentations on similar topic, category or speaker

Interested in talks like this? Follow ESEC-FSE