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.
Wed 6 DecDisplayed time zone: Pacific Time (US & Canada) change
16:00 - 18:00 | Formal VerificationResearch Papers / Industry Papers / Ideas, Visions and Reflections / Demonstrations at Golden Gate C2 Chair(s): Christoph Treude University of Melbourne | ||
16:00 15mTalk | State Merging with Quantifiers in Symbolic Execution Research Papers David Trabish Tel Aviv University, Noam Rinetzky Tel Aviv University, Sharon Shoham Tel Aviv University, Vaibhav Sharma University of Minnesota DOI Pre-print Media Attached | ||
16:15 15mTalk | Towards Strengthening Formal Specifications with Mutation Model Checking Ideas, Visions and Reflections Maxime Cordy SnT, University of Luxembourg, Sami Lazreg SnT, University of Luxembourg, Axel Legay Université Catholique de Louvain, Belgium, Pierre Yves Schobbens University of Namur Media Attached | ||
16:30 15mTalk | PropProof: Free Model-Checking Harnesses from PBT Industry Papers Yoshiki Takashima Carnegie Mellon University DOI Media Attached | ||
16:45 15mTalk | Engineering a Formally Verified Automated Bug Finder Research Papers Arthur Correnson CISPA Helmholtz Center for Information Security, Dominic Steinhöfel CISPA Helmholtz Center for Information Security Media Attached | ||
17:00 15mTalk | LightF3: A Lightweight Fully-Process Formal Framework for Automated Verifying Railway Interlocking Systems Industry Papers Yibo Dong East China Normal University; Shanghai Trusted Industrial Control Platform, Xiaoyu Zhang East China Normal University, Yicong Xu East China Normal University, Chang Cai East China Normal University, Yu Chen East China Normal University, Weikai Miao East China Normal University, Jianwen Li East China Normal University, China, Geguang Pu East China Normal University DOI Media Attached | ||
17:15 15mTalk | Speeding up SMT Solving via Compiler Optimization Research Papers Media Attached | ||
17:30 15mTalk | [Remote] Detecting Atomicity Violations in Interrupt-Driven Programs via Interruption Points Selecting and Delayed ISR-Triggering Research Papers Bin Yu School of Computer Science and Technology, Xidian University, Cong Tian Xidian University, Hengrui Xing School of Computer Science and Technology, Xidian University, Zuchao Yang School of Computer Science and Technology, Xidian University, Jie Su School of Computer Science and Technology, Xidian University, Xu Lu School of Computer Science and Technology, Xidian University, Jiyu Yang School of Computer Science and Technology, Xidian University, Liang Zhao School of Computer Science and Technology, Xidian University, Xiaofeng Li Beijing Institute of Control Engineering, Zhenhua Duan Xidian University Media Attached | ||
17:45 7mTalk | [Remote] P4b: A Translator from P4 Programs to Boogie Demonstrations Media Attached |