High-Level Abstractions for Simplifying Extended String Constraints in SMT

被引：13

作者：

Reynolds, Andrew ^{[1
]}

Notzli, Andres ^{[2
]}

Barrett, Clark ^{[2
]}

Tinelli, Cesare ^{[1
]}

机构：

[1] Univ Iowa, Dept Comp Sci, Iowa City, IA 52242 USA

[2] Stanford Univ, Dept Comp Sci, Stanford, CA 94305 USA

来源：

COMPUTER AIDED VERIFICATION, CAV 2019, PT II | 2019年 / 11562卷

基金：

美国国家科学基金会;

关键词：

D O I：

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

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

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.

引用

页码：23 / 42

页数：20

共 21 条

[1]

Abdulla P.A., 2018, Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30-November 2, 2018, P1, DOI DOI 10.23919/FMCAD.2018.8602997

[2] Syntax-Guided Synthesis [J].

Alur, Rajeev ;

Bodik, Rastislav ;

Dallal, Eric ;

Fisman, Dana ;

Garg, Pranav ;

Juniwal, Garvit ;

Kress-Gazit, Hadas ;

Madhusudan, P. ;

Martin, Milo M. K. ;

Raghothaman, Mukund ;

Saha, Shamwaditya ;

Seshia, Sanjit A. ;

Singh, Rishabh ;

Solar-Lezama, Armando ;

Torlak, Emina ;

Udupa, Abhishek .

DEPENDABLE SOFTWARE SYSTEMS ENGINEERING, 2015, 40 :1-25

[3]

Barrett Clark, 2011, Computer Aided Verification. Proceedings 23rd International Conference, CAV 2011, P171, DOI 10.1007/978-3-642-22110-1_14

[4]

Berzish M, 2017, PROCEEDINGS OF THE 17TH CONFERENCE ON FORMAL METHODS IN COMPUTER AIDED DESIGN (FMCAD 2017), P55, DOI 10.23919/FMCAD.2017.8102241

[5]

Bjorner N, 2009, LECT NOTES COMPUT SC, V5505, P307, DOI 10.1007/978-3-642-00768-2_27

[6]

Chaudhuri S, 2016, LECT NOTES COMPUTER, V9779, DOI [10.1007/978-3-319-41528-4, DOI 10.1007/978-3-319-41528-4]

[7]

Chen T., 2019, PACMPL POPL, V3

[8] Z3: An efficient SMT solver [J].

de Moura, Leonardo ;

Bjorner, Nikolaj .

TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 2008, 4963 :337-340

[9]

Guodong Li, 2013, Hardware and Software: Verification and Testing. 9th International Haifa Verification Conference, HVC 2013. Proceedings: LNCS 8244, P15, DOI 10.1007/978-3-319-03077-7_2

[10] HAMPI: A Solver for Word Equations over Strings, Regular Expressions, and Context-Free Grammars [J].

Kiezun, Adam ;

Ganesh, Vijay ;

Artzi, Shay ;

Guo, Philip J. ;

Hooimeijer, Pieter ;

Ernst, Michael D. .

ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, 2012, 21 (04)

← 1 2 3 →