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
Descripción
Sumario: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.

Ejemplares similares