Publication Details

Solving Not-Substring Constraint with Flat Abstraction

ABDULLA Parosh A., ATIG Mohamed F., BUI Phi Diep, HOLÍK Lukáš, CHEN Yu-Fang and WU Zhilin. Solving Not-Substring Constraint with Flat Abstraction. In: Programming Languages and Systems - 19th Asian Symposium, APLAS 2021, Chicago, IL, USA, October 17-18, 2021, Proceedings. 13008. Berlín: Springer International Publishing, 2021, pp. 305-320. ISBN 978-3-030-89051-3. Available from: https://doi.org/10.1007/978-3-030-89051-3\_17
Czech title
Řešení ne-podřetězcového omezení pomocí ploché abstrakce
Type
conference paper
Language
english
Authors
Abdulla Parosh A. (Uppsala)
Atig Mohamed F. (Uppsala)
Bui Phi Diep (Uppsala)
Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT)
Chen Yu-Fang (ASIN)
Wu Zhilin (Chinese Academy of Sciences)
URL
Keywords

CEGAR, string constraints, strings

Abstract

Not-substring is currently among the least supported types of string constraints, and existing solvers use only relatively crude heuristics. Yet, not-substring occurs relatively often in practical examples and is useful in encoding other types of constraints. In this paper, we propose a systematic way to solve not-substring using the Counter-Example Guided Abstraction Refinement (CEGAR) framework based on flat abstraction. In such a framework, the domain of string variables is restricted to flat languages and subsequently, the whole constraints can be expressed as linear arithmetic formulae. We show that non-substring constraints can be flattened efficiently, and provide experimental evidence that the proposed solution for not-substring is competitive with the state-of-the-art string solvers.

Published
2021
Pages
305-320
Proceedings
Programming Languages and Systems - 19th Asian Symposium, APLAS 2021, Chicago, IL, USA, October 17-18, 2021, Proceedings
Series
13008
Conference
19th Asian Symposium on Programming Languages and Systems -- APLAS'21, Chicago, US
ISBN
978-3-030-89051-3
Publisher
Springer International Publishing
Place
Berlín, DE
DOI
10.1007/978-3-030-89051-3_17
UT WoS
000783821500017
EID Scopus
2-s2.0-85118186762
BibTeX 
@INPROCEEDINGS{FITPUB12676,
   author = "A. Parosh Abdulla and F. Mohamed Atig and Diep Phi Bui and Luk\'{a}\v{s} Hol\'{i}k and Yu-Fang Chen and Zhilin Wu",
   title = "Solving Not-Substring Constraint with Flat Abstraction",
   pages = "305--320",
   booktitle = "Programming Languages and Systems - 19th Asian Symposium, APLAS 2021, Chicago, IL, USA, October 17-18, 2021, Proceedings",
   series = "13008",
   year = 2021,
   location = "Berl\'{i}n, DE",
   publisher = "Springer International Publishing",
   ISBN = "978-3-030-89051-3",
   doi = "10.1007/978-3-030-89051-3\_17",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/12676"
}
Back to top