Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • 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.
Visa övriga samt affilieringar
2014 (Engelska)Ingår i: 26th International Conference on Computer Aided Verification (CAV 2014), Vienna, Austria, Jul. 9-12, 2014., Springer, 2014, 150-166 s.Konferensbidrag, Publicerat paper (Refereegranskat)
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.

Ort, förlag, år, upplaga, sidor
Springer, 2014. 150-166 s.
Serie
Lecture Notes in Computer Science, ISSN 0302-9743 (print), 1611-3349 (online) ; 8559
Nationell ämneskategori
Data- och informationsvetenskap
Identifikatorer
URN: urn:nbn:se:liu:diva-114404DOI: 10.1007/978-3-319-08867-9_10ISBN: 978-3-319-08866-2 (tryckt)ISBN: 978-3-319-08867-9 (tryckt)OAI: oai:DiVA.org:liu-114404DiVA: diva2:789856
Konferens
CAV 2014
Tillgänglig från: 2015-02-20 Skapad: 2015-02-20 Senast uppdaterad: 2016-08-22

Open Access i DiVA

Fulltext saknas

Övriga länkar

Förlagets fulltexthttp://link.springer.com/chapter/10.1007%2F978-3-319-08867-9_10

Sök vidare i DiVA

Av författaren/redaktören
Rezine, Ahmed
Av organisationen
Programvara och systemTekniska högskolan
Data- och informationsvetenskap

Sök vidare utanför DiVA

GoogleGoogle Scholar

Altmetricpoäng

Totalt: 383 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf