Towards String Support in JayHorn (Competition Contribution)

JayHorn is a Horn clause-based model checker for Java programs that has been competing at SV-COMP since 2019. An ongoing research and implementation effort is to add support for String data-type to JayHorn. Since current Horn solvers do not support strings natively, we consider a representation of (...

Descripción completa

Detalles Bibliográficos
Autores principales: Shamakhi, Ali, Hojjat, Hossein, Rümmer, Philipp
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2021
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7984604/
http://dx.doi.org/10.1007/978-3-030-72013-1_29
_version_ 1783668097409875968
author Shamakhi, Ali
Hojjat, Hossein
Rümmer, Philipp
author_facet Shamakhi, Ali
Hojjat, Hossein
Rümmer, Philipp
author_sort Shamakhi, Ali
collection PubMed
description JayHorn is a Horn clause-based model checker for Java programs that has been competing at SV-COMP since 2019. An ongoing research and implementation effort is to add support for String data-type to JayHorn. Since current Horn solvers do not support strings natively, we consider a representation of (unbounded) strings using algebraic data-types, more precisely as lists. This paper discusses Horn clause encodings of different string operations, and presents preliminary results.
format Online
Article
Text
id pubmed-7984604
institution National Center for Biotechnology Information
language English
publishDate 2021
record_format MEDLINE/PubMed
spelling pubmed-79846042021-03-23 Towards String Support in JayHorn (Competition Contribution) Shamakhi, Ali Hojjat, Hossein Rümmer, Philipp Tools and Algorithms for the Construction and Analysis of Systems Article JayHorn is a Horn clause-based model checker for Java programs that has been competing at SV-COMP since 2019. An ongoing research and implementation effort is to add support for String data-type to JayHorn. Since current Horn solvers do not support strings natively, we consider a representation of (unbounded) strings using algebraic data-types, more precisely as lists. This paper discusses Horn clause encodings of different string operations, and presents preliminary results. 2021-02-26 /pmc/articles/PMC7984604/ http://dx.doi.org/10.1007/978-3-030-72013-1_29 Text en © The Author(s) 2021 Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
spellingShingle Article
Shamakhi, Ali
Hojjat, Hossein
Rümmer, Philipp
Towards String Support in JayHorn (Competition Contribution)
title Towards String Support in JayHorn (Competition Contribution)
title_full Towards String Support in JayHorn (Competition Contribution)
title_fullStr Towards String Support in JayHorn (Competition Contribution)
title_full_unstemmed Towards String Support in JayHorn (Competition Contribution)
title_short Towards String Support in JayHorn (Competition Contribution)
title_sort towards string support in jayhorn (competition contribution)
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7984604/
http://dx.doi.org/10.1007/978-3-030-72013-1_29
work_keys_str_mv AT shamakhiali towardsstringsupportinjayhorncompetitioncontribution
AT hojjathossein towardsstringsupportinjayhorncompetitioncontribution
AT rummerphilipp towardsstringsupportinjayhorncompetitioncontribution

Ejemplares similares