Publication Details

Solving String Constraints with Approximate Parikh Image

HOLÍKOVÁ Lenka and JANKŮ Petr. Solving String Constraints with Approximate Parikh Image. In: Proceedings of EUROCAST'19. Lecture Notes in Computer Science. Heidelberg: Springer International Publishing, 2019, pp. 1-8. ISBN 978-3-030-45092-2.
Czech title
Řešení řetězcových omezení pomocí přibližného Parikh Image
Type
conference paper
Language
english
Authors
Holíková Lenka, Ing. (DITS FIT BUT)
Janků Petr, Ing. (DITS FIT BUT)
Keywords

String constraint solving,
Program verification,
Parikh Image,
Alternating Finite Automata,
Decision Procedure

Abstract

In this paper, we propose a refined version of the Parikh image abstraction of finite automata to resolve string length constraints. We integrate this abstraction into the string solver SLOTH, where on top of handling length constraints, our abstraction is also used to speed-up solving other types of constraints. The experimental results show that our extension of SLOTH has good results on simple benchmarks as well as on complex benchmarks that are real-word combinations of transducer and concatenation constraints.

Published
2019
Pages
1-8
Proceedings
Proceedings of EUROCAST'19
Series
Lecture Notes in Computer Science
Conference
Eurocast 2019 -- 17th International Conference on Computer Aided Systems Theory, Las Palmas de Gran Canaria, Canary Islands, ES
ISBN
978-3-030-45092-2
Publisher
Springer International Publishing
Place
Heidelberg, DE
DOI
10.1007/978-3-030-45093-9_59
EID Scopus
2-s2.0-85083999125
BibTeX 
@INPROCEEDINGS{FITPUB12135,
   author = "Lenka Hol\'{i}kov\'{a} and Petr Jank\r{u}",
   title = "Solving String Constraints with Approximate Parikh Image",
   pages = "1--8",
   booktitle = "Proceedings of EUROCAST'19",
   series = "Lecture Notes in Computer Science",
   year = 2019,
   location = "Heidelberg, DE",
   publisher = "Springer International Publishing",
   ISBN = "978-3-030-45092-2",
   doi = "10.1007/978-3-030-45093-9\_59",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/12135"
}
Back to top