Write a Blog >>
ESEC/FSE 2021
Mon 23 - Sat 28 August 2021 Athens, Greece

This program is tentative and subject to change.

Wed 25 Aug 2021 08:40 - 09:00 - Testing—Approximations in Testing and Analysis
Wed 25 Aug 2021 20:40 - 21:00 - Testing—Approximations in Testing and Analysis

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 existence of test oracle problem. To complement existing approaches and overcome their weaknesses, this paper introduces skeletal approximation enumeration (SAE), a novel lightweight and general testing techniques 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. In two months, our approach has found 71 confirmed and unique bugs in Z3 and CVC4, 55 of which have already been fixed.

This program is tentative and subject to change.

Conference Day
Wed 25 Aug

Displayed time zone: Athens change

08:00 - 09:00
Testing—Approximations in Testing and AnalysisResearch Papers +12h
08:00
20m
Talk
Symbolic Parallel Adaptive Importance Sampling for Probabilistic Program Analysis
Research Papers
Yicheng LuoUniversity College London, Antonio FilieriImperial College London, Yuan ZhouArtificial Intelligence Research Center, DII
08:20
20m
Talk
Boosting Static Analysis Accuracy With Instrumented Test Executions
Research Papers
Tianyi ChenUniversity of Southern California, Kihong HeoKAIST, Mukund RaghothamanUniversity of Southern California
08:40
20m
Talk
Skeletal Approximation Enumeration for SMT Solver Testing
Research Papers
Peisen YaoHong Kong University of Science and Technology, Heqing HuangHong Kong University of Science and Technology, Tang WenshengHong Kong University of Science and Technology, Qingkai ShiHong Kong University of Science and Technology, Rongxin WuXiamen University, Charles ZhangHong Kong University of Science and Technology
20:00 - 21:00
Testing—Approximations in Testing and AnalysisResearch Papers
20:00
20m
Talk
Symbolic Parallel Adaptive Importance Sampling for Probabilistic Program Analysis
Research Papers
Yicheng LuoUniversity College London, Antonio FilieriImperial College London, Yuan ZhouArtificial Intelligence Research Center, DII
20:20
20m
Talk
Boosting Static Analysis Accuracy With Instrumented Test Executions
Research Papers
Tianyi ChenUniversity of Southern California, Kihong HeoKAIST, Mukund RaghothamanUniversity of Southern California
20:40
20m
Talk
Skeletal Approximation Enumeration for SMT Solver Testing
Research Papers
Peisen YaoHong Kong University of Science and Technology, Heqing HuangHong Kong University of Science and Technology, Tang WenshengHong Kong University of Science and Technology, Qingkai ShiHong Kong University of Science and Technology, Rongxin WuXiamen University, Charles ZhangHong Kong University of Science and Technology