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)


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
Publication date23 Aug 2022
ISBN (Print)978-3-031-15076-0
ISBN (Electronic)978-3-031-15077-7
Publication statusPublished - 23 Aug 2022
Event28th International Symposium on Model Checking of Software -
Duration: 21 May 202221 May 2022


Conference28th International Symposium on Model Checking of Software
Internet address
SeriesLecture Notes in Computer Science


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

Cite this