ICSE 2020 (series) / ACM Student Research Competition /
Stress Testing SMT Solvers via Type-aware Mutation
Wed 8 Jul 2020 02:10 - 03:00 at SRC Poster Special Room - P305-SRC-Posters
This paper introduces type-aware mutation, a simple, but effective methodology for stress testing Satisfiability Modulo Theories (SMT) solvers. The key idea is mutating the operators of the formula to generate test inputs, while preserving the validity of the mutants by considering the type of the operators. Type-aware mutation was realized and evaluated on finding bugs in two state-of-the-art SMT solvers Z3 and CVC4. During the four months of empirical evaluation, 101 unique, confirmed bugs were found by type-aware mutation, and 87 of them have been fixed. The testing efforts and bugs were well-appreciated by the developers.
Wed 8 JulDisplayed time zone: (UTC) Coordinated Universal Time change
Wed 8 Jul
Displayed time zone: (UTC) Coordinated Universal Time change
02:10 - 03:00 | |||
02:10 50mPoster | Exploring the Relationship between Dockerfile Quality and Project Charateristics ACM Student Research Competition Yiwen Wu National University of Defense Technology | ||
02:10 50mPoster | Towards Automated Migration for Blockchain-based Decentralized Application ACM Student Research Competition Xiufeng Xu Peking University | ||
02:10 50mPoster | Stress Testing SMT Solvers via Type-aware Mutation ACM Student Research Competition Chengyu Zhang East China Normal University | ||
02:10 50mPoster | Does Fixing Bug Increase Robustness in Deep Learning? ACM Student Research Competition Rangeet Pan Iowa State University, USA | ||
02:10 50mPoster | Detection and Mitigation of JIT-Induced Side Channels ACM Student Research Competition Tegan Brennan University of California, Santa Barbara | ||
02:10 50mPoster | Uncertainty-Guided Testing and Robustness Enhancement for Deep Learning Systems ACM Student Research Competition Xiyue Zhang Peking University |