File(s) under embargo

Reason: Publisher requirement.

8

month(s)

until file(s) become available

String theories involving regular membership predicates: from practice to theory and back

conference contribution
posted on 21.07.2021, 15:28 by Murphy Berzish, Joel DayJoel Day, Vijay Ganesh, Mitja Kulczynski, Florin Manea, Federico Mora, Dirk Nowotka
Widespread use of string solvers in formal analysis of stringheavy programs has led to a growing demand for more efficient and reliable techniques which can be applied in this context, especially for real-world cases. Designing an algorithm for the (generally undecidable) satisfiability problem for systems of string constraints requires a thorough understanding of the structure of constraints present in the targeted cases. In this paper, we investigate benchmarks presented in the literature containing regular expression membership predicates, extract different first order logic theories, and prove their decidability, resp. undecidability. Notably, the most common theories in real-world benchmarks are PSPACEcomplete and directly lead to the implementation of a more efficient algorithm to solving string constraints.

History

School

  • Science

Department

  • Computer Science

Published in

Combinatorics on Words. 13th International Conference, WORDS 2021 Rouen, France, September 13–17, 2021. Proceedings. (WORDS 2021)

Pages

50-64

Source

13th International Conference on Words (WORDS 2021)

Publisher

Springer International Publishing

Version

AM (Accepted Manuscript)

Rights holder

© Springer Nature Switzerland AG

Publisher statement

The final authenticated publication is available online at https://doi.org/10.1007/978-3-030-85088-3.

Acceptance date

18/06/2021

Publication date

2021-09-20

Copyright date

2021

ISBN

9783030850876; 9783030850883

Book series

Theoretical Computer Science and General Issues; 12847

Language

en

Editor(s)

Thierry Lecroq; Svetlana Puzynina

Location

Rouen, France (Online)

Event dates

13th September 2021 - 17th September 2021

Depositor

Dr Joel Day. Deposit date: 21 July 2021

Usage metrics

Categories

Exports