Solving String Theories Involving Regular Membership Predicates Using SAT

Mitja Kulczynski, Kevin Lotz*, Dirk Nowotka, Danny Bøgsted Poulsen

*Corresponding author for this work

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

2 Citations (Scopus)

Abstract

String solvers gained a more prominent role in the formal analysis of string-heavy programs, causing an ever-growing need for efficient and reliable solving algorithms. Regular constraints play a central role in several real-world queries. To emerge this field, we present two approaches to encode regular constraints as a Boolean satisfiability problem, one making use of the inductive structure of regular expressions and one working on nondeterministic finite automata. We implement both approaches using Woorpje, a recently developed purely SAT-based string solver, as a framework. An evaluation of our approaches shows that they are competitive to state-of-the-art string solvers and even outperform them in many cases.

Original languageEnglish
Title of host publicationModel Checking Software, SPIN 2022 : 28th International Symposium, SPIN 2022, Proceedings
EditorsOwolabi Legunsen, Grigore Rosu
Number of pages18
Volume13255
PublisherSpringer
Publication date23 Aug 2022
Edition1
Pages134-151
ISBN (Print)978-3-031-15076-0
ISBN (Electronic)978-3-031-15077-7
DOIs
Publication statusPublished - 23 Aug 2022
Event28th International Symposium on Model Checking of Software -
Duration: 21 May 202221 May 2022
https://spin2022chi.web.illinois.edu/

Conference

Conference28th International Symposium on Model Checking of Software
Period21/05/202221/05/2022
Internet address
SeriesLecture Notes in Computer Science
Volume13255
ISSN0302-9743

Fingerprint

Dive into the research topics of 'Solving String Theories Involving Regular Membership Predicates Using SAT'. Together they form a unique fingerprint.

Cite this