Write a Blog >>
Fri 29 May 2020 14:40 - 15:00 at TBD6 - Software Verification

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 model-counting constraint solvers. We focus on strings here, but our approach carries over to other theories and their combinations.

Fri 29 May

14:00 - 15:40: Paper Presentations - Software Verification at TBD6
icse-2020-papers14:00 - 14:20
Martin KelloggUniversity of Washington, Seattle, Manli RanUniversity of California, Riverside, Manu SridharanUniversity of California Riverside, Martin SchäfAmazon Web Services, USA, Michael D. ErnstUniversity of Washington, USA
Demonstrations14:20 - 14:30
Kush JainThe University of Texas at Austin, Karl PalmskogUniversity of Texas at Austin, Ahmet CelikFacebook, Inc., Emilio Jesús Gallego AriasMINES ParisTech, Milos GligoricThe University of Texas at Austin
icse-2020-New-Ideas-and-Emerging-Results14:30 - 14:40
Jude AnilTCS Research, Sumanth PrabhuTCS Research, Kumar MadhukarTCS Innovation Labs (TRDDC), R Venkatesh
icse-2020-papers14:40 - 15:00
Alexandra BugariuETH Zurich, Peter MüllerETH Zurich
icse-2020-Software-Engineering-in-Practice15:00 - 15:20
Nathan ChongAmazon, Byron CookAmazon, Konstantinos KallasUniversity of Pennsylvania, Kareem KhazemAmazon, Felipe R. MonteiroAmazon Web Services, Daniel Schwartz-NarbonneAmazon, n.n., Serdar TasiranAmazon, n.n., Michael TautschnigAmazon Web Services, Mark R. TuttleAmazon
Demonstrations15:20 - 15:30
Zhenbang ChenCollege of Computer, National University of Defense Technology, Changsha, PR China, Hengbiao YuNational University of Defense Technology, Xianjin FuNational University of Defense Technology, Ji WangSchool of Computer, National University of Defense Technology, China
icse-2020-New-Ideas-and-Emerging-Results15:30 - 15:40
Alyas AlmaawiThe University of Texas at Austin, Nima DiniUniversity of Texas at Austin, Cagdas YelenThe University of Texas at Austin, Milos GligoricThe University of Texas at Austin, Sasa MisailovicUniversity of Illinois at Urbana-Champaign, Sarfraz KhurshidUniversity of Texas at Austin