Search: onr:"swepub:oai:DiVA.org:uu-238131" >
String Constraints ...
String Constraints for Verification
-
- Abdulla, Parosh Aziz (author)
- Uppsala universitet,Datorteknik
-
- Atig, Mohamed Faouzi (author)
- Uppsala universitet,Datorteknik
-
- Chen, Yu-Fang (author)
- Institute of Information Science, Academia Sinica
-
show more...
-
- Holik, Lukas (author)
- Brno University
-
- Rezine, Ahmed (author)
- Linköping University
-
- Rümmer, Philipp (author)
- Uppsala universitet,Datorteknik
-
show less...
-
(creator_code:org_t)
- Cham : Springer, 2014
- 2014
- English.
-
In: Computer Aided Verification - 26th International Conference, {CAV} 2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna, Austria, July 18-22, 2014. Proceedings. - Cham : Springer. - 9783319088662 ; , s. 150-166
- Related links:
-
https://urn.kb.se/re...
-
show more...
-
https://doi.org/10.1...
-
show less...
Abstract
Subject headings
Close
- 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.
Subject headings
- TEKNIK OCH TEKNOLOGIER -- Elektroteknik och elektronik -- Datorsystem (hsv//swe)
- ENGINEERING AND TECHNOLOGY -- Electrical Engineering, Electronic Engineering, Information Engineering -- Computer Systems (hsv//eng)
Keyword
- String Solver
- Datavetenskap
- Computer Science
Publication and Content Type
- ref (subject category)
- kon (subject category)
Find in a library
To the university's database