Automatically testing string solvers

Abstract

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.

BibTeX

@inproceedings{Bugariu-Mueller:ICSE20,
  author    = {Alexandra Bugariu and
               Peter M{\"{u}}ller},
  title     = {Automatically testing string solvers},
  booktitle = {ICSE},
  pages     = {1459--1470},
  publisher = {{ACM}},
  year      = {2020},
}

Automatically testing string solvers

Abstract

Related papers