Detail publikačního výsledku

String Constraints for Verification

HOLÍK, L.; ABDULLA, P.; ATIG, M.; CHEN, Y.; RUMMER, P.; STENMAN, J.

Originální název

String Constraints for Verification

Anglický název

String Constraints for Verification

Druh

Stať ve sborníku v databázi WoS či Scopus

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.

Anglický 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

Klíčová slova v angličtině

verification
string
logic

Autoři

HOLÍK, L.; ABDULLA, P.; ATIG, M.; CHEN, Y.; RUMMER, P.; STENMAN, J.

Rok RIV

2015

Vydáno

16.08.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

Svazek

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"
}