High-Level Abstractions for Simplifying Extended String Constraints in SMT

Andrew Reynolds; Andres Notzli; Clark Barrett; Cesare Tinelli

doi:10.1007/978-3-030-25543-5_2

Back

High-Level Abstractions for Simplifying Extended String Constraints in SMT

Conference proceeding

Open access

Peer reviewed

High-Level Abstractions for Simplifying Extended String Constraints in SMT

Andrew Reynolds, Andres Notzli, Clark Barrett and Cesare Tinelli

COMPUTER AIDED VERIFICATION, CAV 2019, PT II, Vol.11562, pp.23-42

Lecture Notes in Computer Science

01/01/2019

DOI: 10.1007/978-3-030-25543-5_2

Files and links (1)

url

https://doi.org/10.1007/978-3-030-25543-5_2View

Published (Version of record) Open Access

Abstract

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.

Computer Science

Technology

Computer Science, Software Engineering

Computer Science, Theory & Methods

Science & Technology

Details

Title: Subtitle: High-Level Abstractions for Simplifying Extended String Constraints in SMT
Creators: Andrew Reynolds - University of Iowa
Andres Notzli - Stanford University
Clark Barrett - Stanford University
Cesare Tinelli - University of Iowa
Contributors: Isil Dillig (Editor)
Serdar Tasiran (Editor)
Resource Type: Conference proceeding
Publication Details: COMPUTER AIDED VERIFICATION, CAV 2019, PT II, Vol.11562, pp.23-42
Series: Lecture Notes in Computer Science
DOI: 10.1007/978-3-030-25543-5_2
ISSN: 0302-9743
eISSN: 1611-3349
Publisher: Springer Nature
Number of pages: 20
Grant note: 1656926 / National Science Foundation; National Science Foundation (NSF) FA8650-18-2-7854 / Defense Advanced Research Projects Agency; United States Department of Defense; Defense Advanced Research Projects Agency (DARPA) Amazon Web Services
Language: English
Date published: 01/01/2019
Academic Unit: Computer Science
Record Identifier: 9984411082102771

Metrics

6 Record Views

13 Times Cited - Web of Science