Write a Blog >>
ICSE 2020
Wed 24 June - Thu 16 July 2020
Fri 10 Jul 2020 07:06 - 07:18 at Baekje - I19-Code Generation and Verification Chair(s): Raffi Khatchadourian

SMT solvers are at the basis of many applications, such as program verification, program synthesis, and test case generation. For all these applications to provide reliable results, SMT solvers must answer queries correctly. However, since they are complex, highly-optimized software systems, ensuring their correctness is challenging. In particular, state-of-the-art testing techniques do not reliably detect when an SMT solver is unsound.

In this paper, we present an automatic approach for generating test cases that reveal soundness errors in the implementations of string solvers, as well as potential completeness and performance issues. We synthesize input formulas that are satisfiable or unsatisfiable by construction and use this ground truth as test oracle. We automatically apply satisfiability-preserving transformations to generate increasingly-complex formulas, which allows us to detect many errors with simple inputs and, thus, facilitates debugging.

The experimental evaluation shows that our technique effectively reveals bugs in the implementation of widely-used SMT solvers and applies also to other types of solvers, such as automata-based solvers. We focus on strings here, but our approach carries over to other theories and their combinations.

Fri 10 Jul
Times are displayed in time zone: (UTC) Coordinated Universal Time change

icse-2020-paper-presentations
07:00 - 08:00: Paper Presentations - I19-Code Generation and Verification at Baekje
Chair(s): Raffi KhatchadourianCity University of New York (CUNY) Hunter College
icse-2020-New-Ideas-and-Emerging-Results07:00 - 07:06
Talk
Jude AnilTCS Research, Sumanth PrabhuTCS Research, Kumar MadhukarTCS Innovation Labs (TRDDC), R Venkatesh
icse-2020-papers07:06 - 07:18
Talk
Alexandra BugariuETH Zurich, Peter MüllerETH Zurich
Pre-print
icse-2020-New-Ideas-and-Emerging-Results07:18 - 07:24
Talk
Djamel Eddine KhelladiCNRS, France, Benoit CombemaleUniversity of Toulouse and Inria, Mathieu Acher(Univ Rennes, Inria, IRISA), Olivier Barais(Univ Rennes, Inria, IRISA)
icse-2020-papers07:24 - 07:36
Talk
Djamel Eddine KhelladiCNRS, France, Benoit CombemaleUniversity of Toulouse and Inria, Mathieu Acher(Univ Rennes, Inria, IRISA), Olivier Barais(Univ Rennes, Inria, IRISA), Jean-Marc JézéquelUniv Rennes - IRISA
icse-2020-Software-Engineering-in-Practice07:36 - 07:48
Talk
Heiko KoziolekABB Corporate Research, Andreas BurgerABB Corporate Research, Marie Platenius-MohrABB Corporate Research, Julius RückertABB Corporate Research, Hadil AbukwaikABB Corporate Research, Raoul JetleyABB, Abdulla PPABB Corporate Research
Pre-print
icse-2020-Software-Engineering-in-Practice07:48 - 08:00
Talk
Nengwen ZhaoTsinghua University, Junjie ChenTianjin University, Xiao PengChina EverBright Bank, Honglin WangBizSeer, Xinya WuBizSeer, Yuanzong ZhangBizSeer, Zikai ChenTsinghua University, Xiangzhong ZhengBizSeer, Xiaohui NieTsinghua University, Gang WangChina EverBright Bank, Yong WuChina EverBright Bank, Fang ZhouChina EverBright Bank, Wenchi ZhangBizSeer, Kaixin SuiBizSeer, Dan PeiTsinghua University