A Decision Procedure for String Logic with Quadratic Equations, Regular Expressions and Length Constraints

Quang Loc Le, Mengda He

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    110 Downloads (Pure)

    Abstract

    In this work, we consider the satisfiability problem in a logic that combines word equations over string variables denoting words of unbounded lengths, regular languages to which words belong and Presburger constraints on the length of words. We present a novel decision procedure over two decidable fragments that include quadratic word equations (i.e., each string variable occurs at most twice). The proposed procedure reduces the problem to solving the satisfiability in the Presburger arithmetic. The procedure combines two main components: (i) an algorithm to derive a complete set of all solutions of conjunctions of word equations and regular expressions; and (ii) two methods to precisely compute relational constraints over string lengths implied by the set of all solutions. We have implemented a prototype tool and evaluated it over a set of satisfiability problems in the logic. The experimental results show that the tool is effective and efficient.
    Original languageEnglish
    Title of host publicationProgramming Languages and Systems. APLAS 2018
    EditorsS Ryu
    PublisherSpringer
    ISBN (Electronic)9783030027681
    ISBN (Print)9783030027674
    DOIs
    Publication statusPublished - 23 Oct 2018
    Event16th Asian Symposium on Programming Languages and Systems - Wellington, New Zealand
    Duration: 3 Dec 20185 Dec 2018
    http://aplas2018.org

    Publication series

    Name Lecture Notes in Computer Science
    Volume11275
    ISSN (Electronic)1867-822X

    Conference

    Conference16th Asian Symposium on Programming Languages and Systems
    Abbreviated titleAPLAS 2018
    Country/TerritoryNew Zealand
    CityWellington
    Period3/12/185/12/18
    Internet address

    Fingerprint

    Dive into the research topics of 'A Decision Procedure for String Logic with Quadratic Equations, Regular Expressions and Length Constraints'. Together they form a unique fingerprint.

    Cite this