Skeletal Approximation Enumeration for SMT Solver Testing
Wed 25 Aug 2021 20:00 - 20:10 - Testing—Approximations in Testing and Analysis Chair(s): Shane McIntosh
Ensuring the equality of SMT solvers is critical due to its broad spectrum of applications in academia and industry, such as symbolic execution and program verification. Existing approaches to testing SMT solvers are either too costly or find difficulties generalizing to different solvers and theories, due to the test oracle problem. To complement existing approaches and overcome their weaknesses, this paper introduces skeletal approximation enumeration (SAE), a novel lightweight and general testing technique for all first-order theories. To demonstrate its practical utility, we have applied the SAE technique to test Z3 and CVC4, two comprehensively tested, state-of-the-art SMT solvers. By the time of writing, our approach had found 71 confirmed bugs in Z3 and CVC4,55 of which had already been fixed.
Wed 25 AugDisplayed time zone: Athens change
08:00 - 09:00 | Testing—Approximations in Testing and AnalysisResearch Papers +12h Chair(s): Mike Papadakis University of Luxembourg | ||
08:00 10mPaper | Skeletal Approximation Enumeration for SMT Solver Testing Research Papers Peisen Yao Hong Kong University of Science and Technology, Heqing Huang Hong Kong University of Science and Technology, Wensheng Tang Hong Kong University of Science and Technology, Qingkai Shi Purdue University, Rongxin Wu Xiamen University, Charles Zhang Hong Kong University of Science and Technology DOI | ||
08:10 10mPaper | Boosting Static Analysis Accuracy with Instrumented Test Executions Research Papers Tianyi Chen University of Southern California, Kihong Heo KAIST, Mukund Raghothaman University of Southern California DOI | ||
08:20 10mPaper | Symbolic Parallel Adaptive Importance Sampling for Probabilistic Program Analysis Research Papers Yicheng Luo University College London, Antonio Filieri Imperial College London, Yuan Zhou University of Oxford DOI | ||
08:30 30mLive Q&A | Q&A (Testing—Approximations in Testing and Analysis) Research Papers | ||
20:00 - 21:00 | Testing—Approximations in Testing and AnalysisResearch Papers Chair(s): Shane McIntosh McGill University | ||
20:00 10mPaper | Skeletal Approximation Enumeration for SMT Solver Testing Research Papers Peisen Yao Hong Kong University of Science and Technology, Heqing Huang Hong Kong University of Science and Technology, Wensheng Tang Hong Kong University of Science and Technology, Qingkai Shi Purdue University, Rongxin Wu Xiamen University, Charles Zhang Hong Kong University of Science and Technology DOI | ||
20:10 10mPaper | Boosting Static Analysis Accuracy with Instrumented Test Executions Research Papers Tianyi Chen University of Southern California, Kihong Heo KAIST, Mukund Raghothaman University of Southern California DOI | ||
20:20 10mPaper | Symbolic Parallel Adaptive Importance Sampling for Probabilistic Program Analysis Research Papers Yicheng Luo University College London, Antonio Filieri Imperial College London, Yuan Zhou University of Oxford DOI | ||
20:30 30mLive Q&A | Q&A (Testing—Approximations in Testing and Analysis) Research Papers | ||