“High-Level Abstractions for Simplifying Extended String Constraints in SMT” by Andrew Reynolds, Andres Nötzli, Clark Barrett, and Cesare Tinelli. In Proceedings of the 31^st International Conference on Computer Aided Verification (CAV '19), (Isil Dillig and Serdar Tasiran, eds.), July 2019, pp. 23-42. New York, New York.
Satisfiability Modulo Theories (SMT) solvers with support for the theory of strings have recently emerged as powerful tools for reasoning about string-manipulating programs. However, due to the complex semantics of extended string functions, it is challenging to develop scalable solvers for the string constraints produced by program analysis tools. We identify several classes of simplification techniques that are critical for the efficient processing of string constraints in SMT solvers. These techniques can reduce the size and complexity of input constraints by reasoning about arithmetic entailment, multisets, and string containment relationships over input terms. We provide experimental evidence that implementing them results in significant improvements over the performance of state-of-the-art SMT solvers for extended string constraints.
BibTeX entry:
@inproceedings{RNB+19,
author = {Andrew Reynolds and Andres N{\"o}tzli and Clark Barrett and
Cesare Tinelli},
editor = {Isil Dillig and Serdar Tasiran},
title = {High-Level Abstractions for Simplifying Extended String
Constraints in {SMT}},
booktitle = {Proceedings of the {\it 31^{st}} International Conference
on Computer Aided Verification (CAV '19)},
series = {Lecture Notes in Computer Science},
volume = {11561},
pages = {23--42},
publisher = {Springer International Publishing},
month = jul,
year = {2019},
isbn = {978-3-030-25542-8},
doi = {10.1007/978-3-030-25543-5_2},
note = {New York, New York},
url = {http://theory.stanford.edu/~barrett/pubs/RNB+19.pdf}
}
(This webpage was created with bibtex2web.)