Publication Details

String Constraints for Verification

ABDULLA Parosh A., ATIG Mohamed F., HOLÍK Lukáš, CHEN Yu-Fang, RUMMER Philipp and STENMAN Jari. String Constraints for Verification. In: 26th International Conference on Computer Aided Verification. Lecture Notes in Computer Science, Volume 8559, vol. 8559. Berlin: Springer Verlag, 2014, pp. 150-166. ISBN 978-3-319-08866-2. Available from: http://link.springer.com/chapter/10.1007/978-3-319-08867-9_10
Czech title
Logika nad řetězci s použitím ve verifikaci
Type
conference paper
Language
english
Authors
Abdulla Parosh A. (Uppsala)
Atig Mohamed F. (Uppsala)
Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT)
Chen Yu-Fang (ASIN)
Rummer Philipp (Uppsala)
Stenman Jari (Uppsala)
URL
Keywords

verification
string
logic

Abstract

We present a decision procedure for a logic that combines
(i) word equations over string variables denoting words of arbitrary
lengths, together with (ii) constraints on the length of words, and on (iii) the regular languages to which words belong. Decidability of this general logic is still open. Our procedure is sound for the general logic, and a decision procedure for a particularly rich fragment that restricts the form in which word equations are written. In contrast to many existing procedures, our method does not make assumptions about the maximum length of words. We have developed a prototypical implementation of our decision procedure, and integrated it into a CEGAR-based model checker for the analysis of programs encoded as Horn clauses. Our tool is able to automatically establish the correctness of several programs
that are beyond the reach of existing methods.

Published
2014
Pages
150-166
Proceedings
26th International Conference on Computer Aided Verification
Series
Lecture Notes in Computer Science, Volume 8559
Volume
8559
Conference
26th International Conference on Computer Aided Verification -- CAV 2014, Vídeň, AT
ISBN
978-3-319-08866-2
Publisher
Springer Verlag
Place
Berlin, DE
DOI
10.1007/978-3-319-08867-9_10
UT WoS
000491474200010
EID Scopus
2-s2.0-84904815514
BibTeX 
@INPROCEEDINGS{FITPUB10699,
   author = "A. Parosh Abdulla and F. Mohamed Atig and Luk\'{a}\v{s} Hol\'{i}k and Yu-Fang Chen and Philipp Rummer and Jari Stenman",
   title = "String Constraints for Verification",
   pages = "150--166",
   booktitle = "26th International Conference on Computer Aided Verification",
   series = "Lecture Notes in Computer Science, Volume 8559",
   volume = 8559,
   year = 2014,
   location = "Berlin, DE",
   publisher = "Springer Verlag",
   ISBN = "978-3-319-08866-2",
   doi = "10.1007/978-3-319-08867-9\_10",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/10699"
}
Back to top