Write a Blog >>
ASE 2021
Sun 14 - Sat 20 November 2021 Australia
Tue 16 Nov 2021 19:00 - 19:20 at Koala - Using Knowledge Chair(s): Dalal Alrajeh

Many modern software engineering tools integrate SMT decision procedures and rely on the accuracy and performance of SMT solvers. We describe four basic patterns for integrating constraint solvers (earliest verdict, majority vote, feature-based solver selection, and verdict-based second attempt) that can be used for combining individual solvers into meta-decision procedures that balance accuracy, performance, and cost – or optimize for one of these metrics. In order to evaluate the effectiveness of meta-solving, we analyze and minimize $16$ existing benchmark suites and benchmark seven state-of-the-art SMT solvers on $17k$ unique instances. From the obtained performance data, we can estimate the performance of different meta-solving strategies. We validate our results by implementing and analyzing one strategy. As additional results, we obtain (a) the first benchmark suite of unique SMT string problems with validated expected verdicts, (b) an extensive dataset containing data on benchmark instances as well as on the performance of individual decision procedures and several meta-solving strategies on these instances, and (c) a framework for generating data that can easily be used for similar analyses on different benchmark instances or for different decision procedures.

Tue 16 Nov

Displayed time zone: Hobart change

19:00 - 20:00
Using KnowledgeResearch Papers at Koala
Chair(s): Dalal Alrajeh Imperial College London
19:00
20m
Talk
Data-Driven Design and Evaluation of SMT Meta-Solving Strategies: Balancing Performance, Accuracy, and CostACM Distinguished Paper
Research Papers
Malte Mues TU Dortmund University, Falk Howar TU Dortmund University
19:20
20m
Talk
Reducing Bug Triaging Confusion by Learning from Mistakes with a Bug Tossing Knowledge GraphACM Distinguished Paper
Research Papers
Yanqi Su Australian National University, Zhenchang Xing Australian National University, Xin Peng Fudan University, Xin Xia Huawei Software Engineering Application Technology Lab, Chong Wang Fudan University, Xiwei (Sherry) Xu CSIRO’s Data61, Liming Zhu CSIRO’s Data61; UNSW
19:40
20m
Talk
ASE: A Value Set Decision Procedure for Symbolic Execution
Research Papers
Alireza S. Abyaneh University of Salzburg, Christoph Kirsch University of Salzburg; Czech Technical University
Pre-print