Přístupnostní navigace
E-přihláška
Vyhledávání Vyhledat Zavřít
Detail publikace
HOLÍK, L. ABDULLA, P. ATIG, M. CHEN, Y. RUMMER, P. STENMAN, J.
Originální název
String Constraints for Verification
Typ
článek ve sborníku ve WoS nebo Scopus
Jazyk
angličtina
Originální abstrakt
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.
Klíčová slova
verification string logic
Autoři
HOLÍK, L.; ABDULLA, P.; ATIG, M.; CHEN, Y.; RUMMER, P.; STENMAN, J.
Rok RIV
2014
Vydáno
16. 8. 2014
Nakladatel
Springer Verlag
Místo
Berlin
ISBN
978-3-319-08866-2
Kniha
26th International Conference on Computer Aided Verification
Edice
Lecture Notes in Computer Science, Volume 8559
Strany od
150
Strany do
166
Strany počet
17
URL
http://link.springer.com/chapter/10.1007/978-3-319-08867-9_10
BibTex
@inproceedings{BUT111639, author="Lukáš {Holík} and Parosh {Abdulla} and Mohamed {Atig} and Yu-Fang {Chen} and Philipp {Rummer} and Jari {Stenman}", title="String Constraints for Verification", booktitle="26th International Conference on Computer Aided Verification", year="2014", series="Lecture Notes in Computer Science, Volume 8559", volume="8559", pages="150--166", publisher="Springer Verlag", address="Berlin", doi="10.1007/978-3-319-08867-9\{_}10", isbn="978-3-319-08866-2", url="http://link.springer.com/chapter/10.1007/978-3-319-08867-9_10" }