liu.seSearch for publications in DiVA
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
String Constraints for Verification
Department of Information Technology, Uppsala University, Sweden.
Department of Information Technology, Uppsala University, Sweden.
Institute of Information Science, Academia Sinica, Taiwan.
Faculty of Information Technology, Brno University of Technology, Czech Republic.
Show others and affiliations
2014 (English)In: 26th International Conference on Computer Aided Verification (CAV 2014), Vienna, Austria, Jul. 9-12, 2014., Springer, 2014, 150-166 p.Conference paper, Published paper (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
Springer, 2014. 150-166 p.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 (print), 1611-3349 (online) ; 8559
National Category
Computer and Information Science
Identifiers
URN: urn:nbn:se:liu:diva-114404DOI: 10.1007/978-3-319-08867-9_10ISBN: 978-3-319-08866-2 (print)ISBN: 978-3-319-08867-9 (print)OAI: oai:DiVA.org:liu-114404DiVA: diva2:789856
Conference
CAV 2014
Available from: 2015-02-20 Created: 2015-02-20 Last updated: 2016-08-22

Open Access in DiVA

No full text

Other links

Publisher's full texthttp://link.springer.com/chapter/10.1007%2F978-3-319-08867-9_10

Authority records BETA

Rezine, Ahmed

Search in DiVA

By author/editor
Rezine, Ahmed
By organisation
Software and SystemsThe Institute of Technology
Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 385 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf