Data-Driven Design and Evaluation of SMT Meta-Solving Strategies

Abstract

The 36th IEEE/ACM International Conference on Automated Software Engineering (2021) accepted the paper ‘Data-Driven Design and Evaluation of SMT Meta-Solving Strategies: Balancing Performance, Accuracy, and Cost’ [MH21a] and selected it for an ACM SIGSOFT Distinguished Paper Award. The paper presents four generally applicable patterns for the combination of multiple SMT decision procedures in a meta-solving strategy and demonstrates how a meta-solving strategy for string constraints can be developed in a data-driven approach based on these patterns: The paper cleans up and merges existing collections of SMT benchmarks in string theory solving to evaluate and compare derived meta-solving strategies. Notably, we can demonstrate on the available data that commonly used strategies as earliest returning SMT solver do not always return the most reliable result if all available SMT solvers are combined. Instead, cross-checking strategies work slightly better at moderate overhead.