Solving String Theories Involving Regular Membership Predicates Using SAT

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

*Kontaktforfatter

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

2 Citationer (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.

OriginalsprogEngelsk
TitelModel Checking Software, SPIN 2022 : 28th International Symposium, SPIN 2022, Proceedings
RedaktørerOwolabi Legunsen, Grigore Rosu
Antal sider18
Vol/bind13255
ForlagSpringer
Publikationsdato23 aug. 2022
Udgave1
Sider134-151
ISBN (Trykt)978-3-031-15076-0
ISBN (Elektronisk)978-3-031-15077-7
DOI
StatusUdgivet - 23 aug. 2022
Begivenhed28th International Symposium on Model Checking of Software -
Varighed: 21 maj 202221 maj 2022
https://spin2022chi.web.illinois.edu/

Konference

Konference28th International Symposium on Model Checking of Software
Periode21/05/202221/05/2022
Internetadresse
NavnLecture Notes in Computer Science
Vol/bind13255
ISSN0302-9743

Fingeraftryk

Dyk ned i forskningsemnerne om 'Solving String Theories Involving Regular Membership Predicates Using SAT'. Sammen danner de et unikt fingeraftryk.

Citationsformater