Portal de Periódicos da CAPES

Towards String Support in JayHorn (Competition Contribution)

2021; Springer Science+Business Media; Linguagem: Inglês

10.1007/978-3-030-72013-1_29

1611-3349

Ali Shamakhi, Hossein Hojjat, Philipp Rümmer,

Software Engineering Research

Abstract 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 data-type to . 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.