Search: onr:"swepub:oai:DiVA.org:uu-429864" >
A Decision Procedur...
A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type
-
- Chen, Taolue (author)
- University of Surrey, UK
-
- Hague, Matthew (author)
- Royal Holloway, University of London, UK
-
- He, Jinlong (author)
- State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, China
-
show more...
-
- Hu, Denghang (author)
- State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, China
-
- Lin, Anthony Widjaja (author)
- Technical University of Kaiserslautern, Germany
-
- Rümmer, Philipp, 1978- (author)
- Uppsala universitet,Avdelningen för datorteknik,Datorteknik,Embedded Systems
-
- Wu, Zhilin (author)
- State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, China
-
show less...
-
(creator_code:org_t)
- 2020-10-12
- 2020
- English.
-
In: ATVA 2020. - Cham : Springer Nature. - 9783030591519 - 9783030591526 ; , s. 325-342
- Related links:
-
http://arxiv.org/pdf...
-
show more...
-
https://urn.kb.se/re...
-
https://doi.org/10.1...
-
show less...
Abstract
Subject headings
Close
- In this paper, we propose a decision procedure for a class of string-manipulating programs which includes not only a wide range of string operations such as concatenation, replaceAll, reverse, and finite transducers, but also those involving the integer data-type such as length, indexof, and substring. To the best of our knowledge, this represents one of the most expressive string constraint languages that is currently known to be decidable. Our decision procedure is based on a variant of cost register automata. We implement the decision procedure, giving rise to a new solver OSTRICH+. We evaluate the performance of OSTRICH+ on a wide range of existing and new benchmarks. The experimental results show that OSTRICH+ is the first string decision procedure capable of tackling finite transducers and integer constraints, whilst its overall performance is comparable with the state-of-the-art string constraint solvers.
Subject headings
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
Keyword
- Computer Science
- Datavetenskap
Publication and Content Type
- ref (subject category)
- kon (subject category)
Find in a library
-
ATVA 2020
(Search for host publication in LIBRIS)
To the university's database