Compiler Optimization-Based SMT Simplifications: An In-Depth Study
SMT solvers are a cornerstone in numerous domains, such as program verification, repair, and synthesis. While formula simplification is a crucial preprocessing step that directly impacts solver efficiency, existing approaches predominantly rely on handcrafted heuristics. Recent advances have explored using compiler optimizations to automate and enhance formula simplifications. Despite their promise, the synergy between compiler optimizations and SMT simplifications remains insufficiently understood and underexploited. This paper presents a comprehensive study of the interplay between compiler optimizations and SMT formula simplifications. We show that iterative search for optimization configurations significantly improves formula simplifications, yielding a geometric mean speed-up of 2.96× over default solvers and 2.12× over SLOT on large-scale benchmarks. We present strong evidence for the effectiveness of machine learning-based methods in automating the selection of optimization configurations tailored to specific problem instances, achieving geometric mean speed-ups of 1.15× over Z3 and 1.54× over CVC5. Finally, we discuss promising directions for improving the applicability and effectiveness of compiler optimization-driven approaches to SMT simplifications.
Tue 7 JulDisplayed time zone: Eastern Time (US & Canada) change
16:00 - 17:40 | Verification 1Research Papers / Tool Demonstrations / Journal-First Paper / Ideas, Visions and Reflections at MB 2.430 Chair(s): Charles Zhang Hong Kong University of Science and Technology | ||
16:00 10mTalk | IDPVerifier: Verifying Interrupt-driven Programs Efficiently via Heuristic and Reduced Partial-order Constraints Ideas, Visions and Reflections Zixuan Yuan Xidian University, Bin Yu Xidian University, Xu Lu Xidian University, WenSheng Wang Xidian University, Yuanzhe Liu Xidian University, Cheng Wen Xidian University, Meng Wang Hebei university, Chu Chen Qufu Normal University | ||
16:10 20mTalk | Active Learning of Symbolic Automata for Reactive Programs via Dynamic Symbolic Mapper Research Papers DOI File Attached | ||
16:30 20mTalk | Precondition Synthesis for Deep Neural Networks with Statistical Guarantees Research Papers Zengyu Liu National University of Defense Technology, Bai Xue Institute of Software at Chinese Academy of Sciences, China, Pengfei Yang College of Computer and Information Science, Software College, Southwest University, Ji Wang National University of Defense Technology | ||
16:50 10mTalk | EquivFusion: Unifying Hardware Equivalence Checking from Algorithms to Netlists via MLIR Tool Demonstrations Jiaying Zhu The Chinese University of Hong Kong, Baoqi Zhang National Center of Technology Innovation for EDA, Mengxia Tao National Center of Technology Innovation for EDA, Kezhi Li The Chinese University of Hong Kong, Hao Yan Central South University, Xu, Qiang , Min Li Southeast University | ||
17:00 20mTalk | Compiler Optimization-Based SMT Simplifications: An In-Depth Study Journal-First Paper Hanyun Jiang The State Key Laboratory of Blockchain and Data Security, Zhejiang University, Peisen Yao Zhejiang University, Jiachen Lu The State Key Laboratory of Blockchain and Data Security, Zhejiang University, Yongwang Zhao The State Key Laboratory of Blockchain and Data Security, Zhejiang University, Kui Ren The State Key Laboratory of Blockchain and Data Security, Zhejiang University | ||