String Constraints with Concatenation and Transducers
Solved Efficiently (Technical Report)LUKÁŠ HOLÍK, Brno University of Technology, Czech Republic
PETR JANKŮ, Brno University of Technology, Czech Republic
ANTHONY W. LIN, University of Oxford, United Kingdom
PHILIPP RÜMMER, Uppsala University, SwedenTOMÁŠ VOJNAR, Brno University of Technology, Czech Republic
String analysis is the problem of reasoning about how strings are manipulated by a program. It has numerous
applications including automatic detection of cross-site scripting, and automatic test-case generation. A popularstring analysis technique includes symbolic executions, which at their core use constraint solvers over thestring domain, a.k.a. string solvers. Such solvers typically reason about constraints expressed in theories
over strings with the concatenation operator as an atomic constraint. In recent years, researchers started torecognise the importance of incorporating the replace-all operator (i.e. replace all occurrences of a string byanother string) and, more generally, finite-state transductions in the theories of strings with concatenation.
Such string operations are typically crucial for reasoning about XSS vulnerabilities in web applications,especially for modelling sanitisation functions and implicit browser transductions (e.g. innerHTML). Although
this results in an undecidable theory in general, it was recently shown that the straight-line fragment of thetheory is decidable, and is sufficiently expressive in practice. In this paper, we provide the first string solver thatcan reason about constraints involving both concatenation and finite-state transductions. Moreover, it has acompleteness and termination guarantee for several important fragments (e.g. straight-line fragment). The main
challenge addressed in the paper is the prohibitive worst-case complexity of the theory (double-exponentialtime), which is exponentially harder than the case without finite-state transductions. To this end, we propose
a method that exploits succinct alternating finite-state automata as concise symbolic representations of string
constraints. In contrast to previous approaches using nondeterministic automata, alternation offers not only
exponential savings in space when representing Boolean combinations of transducers, but also a possibilityof succinct representation of otherwise costly combinations of transducers and concatenation. Reasoning
about the emptiness of the AFA language requires a state-space exploration in an exponential-sized graph, forwhich we use model checking algorithms (e.g. IC3). We have implemented our algorithm and demonstrated its
efficacy on benchmarks that are derived from cross-site scripting analysis and other examples in the literature.
Additional Key Words and Phrases: String Solving, Alternating Finite Automata, Decision Procedure, IC3
Authors’ addresses: Lukáš Holík, Brno University of Technology, Faculty of Information Technology, IT4Innovations
Centre of Excellence, Božetěchova 2, Brno, CZ-61266, Czech Republic, holik@fit.vutbr.cz; Petr Janků, Brno University ofTechnology, Faculty of Information Technology, IT4Innovations Centre of Excellence, Božetěchova 2, Brno, CZ-61266,
Czech Republic, ijanku@fit.vutbr.cz; Anthony W. Lin, Department of Computer Science, University of Oxford, Wolfson
Building, Parks Road, Oxford, OX1 3QD, United Kingdom, anthony.lin@cs.ox.ac.uk; Philipp Rümmer, Department ofInformation Technology, Uppsala University, Box 337, Uppsala, 75105, Sweden, philipp.ruemmer@it.uu.se; Tomáš Vojnar,
Brno University of Technology, Faculty of Information Technology, IT4Innovations Centre of Excellence, Božetěchova 2,
Brno, CZ-61266, Czech Republic, vojnar@fit.vutbr.cz.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee
provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and thefull citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored.
Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires
prior specific permission and/or a fee. Request permissions from permissions@acm.org.
© 2018 Copyright held by the owner/author(s). Publication rights licensed to the Association for Computing Machinery.
2475-1421/2018/1-ART4
https://doi.org/10.1145/3158092

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 4. Publication date: January 2018.

4

ACM Reference Format:
Lukáš Holík, Petr Janků, Anthony W. Lin, Philipp Rümmer, and Tomáš Vojnar. 2018. String Constraints with
Concatenation and Transducers Solved Efficiently (Technical Report). Proc. ACM Program. Lang. 2, POPL,
Article 4 (January 2018), 33 pages. https://doi.org/10.1145/3158092

1

INTRODUCTION

Strings are a fundamental data type in many programming languages. This statement is true
now more than ever, especially owing to the rapidly growing popularity of scripting languages(e.g. JavaScript, Python, PHP, and Ruby) wherein programmers tend to make heavy use of string
variables. String manipulations are often difficult to reason about automatically, and could easily
lead to unexpected programming errors. In some applications, some of these errors could haveserious security consequences, e.g., cross-site scripting (a.k.a. XSS), which are ranked among the
top three classes of web application security vulnerabilities by OWASP [OWASP 2013].
Popular methods for analysing how strings are being manipulated by a program include symbolic
executions [Bjørner et al. 2009; Cadar et al. 2008, 2011; Godefroid et al. 2005; Kausler and Sherman
2014; Loring et al. 2017; Redelinghuys et al. 2012; Saxena et al. 2010; Sen et al. 2013] which at theircore use constraint solvers over the string domain (a.k.a. string solvers). String solvers have been
the subject of numerous papers in the past decade, e.g., see [Abdulla et al. 2014; Balzarotti et al.
2008; Barrett et al. 2016; Bjørner et al. 2009; D’Antoni and Veanes 2013; Fu and Li 2010; Fu et al.
2013; Ganesh et al. 2013; Hooimeijer et al. 2011; Hooimeijer and Weimer 2012; Kiezun et al. 2012;
Liang et al. 2014, 2016, 2015; Lin and Barceló 2016; Saxena et al. 2010; Trinh et al. 2014, 2016; Veanes
et al. 2012; Wassermann et al. 2008; Yu et al. 2010, 2014, 2009, 2011; Zheng et al. 2013] among manyothers. As is common in constraint solving, we follow the standard approach of Satisfiability Modulo
Theories (SMT) [De Moura and Bjørner 2011], which is an extension of the problem of satisfiabilityof Boolean formulae wherein each atomic proposition can be interpreted over some logical theories(typically, quantifier-free).
Unlike the case of constraints over integer/real arithmetic (where many decidability and undecidability results are known and powerful algorithms are already available, e.g., the simplex
algorithm), string constraints are much less understood. This is because there are many different
string operations that can be included in a theory of strings, e.g., concatenation, length comparisons,regular constraints (matching against a regular expression), and replace-all (i.e. replacing every
occurrence of a string by another string). Even for the theory of strings with the concatenation
operation alone, existing string solver cannot handle the theory (in its full generality) in a soundand complete manner, despite the existence of a theoretical decision procedure for the problem[Diekert 2002; Gutiérrez 1998; Jez 2016; Makanin 1977; Plandowski 2004, 2006]. This situation isexacerbated when we add extra operations like string-length comparisons, in which case evendecidability is a long-standing open problem [Ganesh et al. 2013]. In addition, recent works in string
solving have argued in favour of adding the replace-all operator or, more generally finite-statetransducers, to string solvers [Lin and Barceló 2016; Trinh et al. 2016; Yu et al. 2010, 2014] in viewof their importance for modelling relevant sanitisers (e.g. backslash-escape) and implicit browser
transductions (e.g. an application of HTML-unescape by innerHTML), e.g., see [D’Antoni and
Veanes 2013; Hooimeijer et al. 2011; Veanes et al. 2012] and Example 1.1 below. However, naively
combining the replace-all operator and concatenation yields undecidability [Lin and Barceló 2016].
Example 1.1. The following JavaScript snippet—an adaptation of an example from [Kern 2014;
Lin and Barceló 2016]—shows use of both concatenation and finite-state transducers:
var x = goog.string.htmlEscape(name);
var y = goog.string.escapeString(x);nameElem.innerHTML = '<button onclick= "viewPerson(\'' + y + '\')">' + x + '</button>';2

The code assigns an HTML markup for a button to the DOM element nameElem. Upon click, thebutton will invoke the function viewPerson on the input name whose value is an untrusted variable.
The code attempts to first sanitise the value of name. This is done via The Closure Library [co 2015]
string functions htmlEscape and escapeString. Inputting the value Tom & Jerry into name gives
the desired HTML markup:<button onclick="viewPerson('Tom &amp; Jerry')">Tom &amp; Jerry</button>

On the other hand, inputting value ');attackScript();// to name, results in the markup:<button onclick="viewPerson('&#39;);attackScript();//')">&#39;);attackScript();//')</button>

Before this string is inserted into the DOM via innerHTML, an implicit browser transduction willtake place [Heiderich et al. 2013; Weinberger et al. 2011], i.e., HTML-unescaping the string inside
the onclick attribute and then invoking the attacker’s script attackScript() after viewPerson.
This subtle DOM-based XSS bug is due to calling the right escape functions, but in wrong order. □One theoretically sound approach proposed in [Lin and Barceló 2016] for overcoming theundecidability of string constraints with both concatenation and finite-state transducers is to
impose a straight-line restriction on the shape of constraints. This straight-line fragment can beconstrued as the problem of path feasibility [Bjørner et al. 2009] in the following simple imperative
language (with only assignment, skip, and assert) for defining non-branching and non-looping
string-manipulating programs that are generated by symbolic execution:
S ::= y := a | assert(b) | skip | S 1 ; S 2 ,a ::= f (x 1 , . . . , x n ),b ::= д(x 1 )where f : (Σ∗ ) n → Σ∗ is either an application of concatenation x 1 ◦ · · · ◦ x n or an applicationof a finite-state transduction R(x 1 ), and д tests membership of x 1 in a regular language. Here,some variables are undefined “input variables”. Path feasibility asks if there exist input strings thatsatisfy all assertions and applications of transductions in the program. It was shown in [Lin andBarceló 2016] that such a path feasibility problem (equivalently, satisfiability for the aforementioned
straight-line fragment) is decidable. As noted in [Lin and Barceló 2016] such a fragment can express
the program logic of many interesting examples of string-manipulating programs with/without
XSS vulnerabilities. For instance, the above example can be modelled as a straight-line formulawhere the regular constraint comes from an attack pattern like the one below:
e1 = /<button onclick="viewPerson\(' ( ' | [^']*[^'\\] ' ) \); [^']*[^'\\]' \)">.*<\/button>/
Unfortunately, the decidability proof given in [Lin and Barceló 2016] provides only a theoreticalargument for decidability and complexity upper bounds (an exponential-time reduction to theacyclic fragment of intersection of rational relations1 whose decidability proof in turn is a highly
intricate polynomial-space procedure using Savitch’s trick [Barceló et al. 2013]) and does not yield
an implementable solution. Furthermore, despite its decidability, the string logic has a prohibitively
high complexity (EXPSPACE-complete, i.e., exponentially higher than without transducers), which
could severely limit its applicability.
Contributions. Our paper makes the following contributions to overcome the above challenges:(1) We propose a fast reduction of satisfiability of formulae in the straight-line fragment and in
the acyclic fragment to the emptiness problem of alternating finite-state automata (AFAs).
The reduction is in the worst case exponential in the number of concatenation operations2 ,1 This fragment consists of constraints that are given as conjunctions of transducers Vm R (x , y ), wherein the graph G
i =1 i i iof variables does not contain a cycle. The graph G contains vertices corresponding to variables x i , yi and that two variables

x, y are linked by an edge if x = x i and y = yi for some i ∈ {1, . . . , m }.
2 This is an unavoidable computational limit imposed by EXPSPACE-hardness of the problem [Lin and Barceló 2016].

3

but otherwise polynomial in the size of a formula. In combination with fast model checking
algorithms (e.g. IC3 [Bradley 2012]) to decide AFA emptiness, this yields the first practicalalgorithm for handling string constraints with concatenation, finite-state transducers (hence,
also replace-all), and regular constraints, and a decision procedure for formulae within thestraight-line and acyclic fragments.
(2) We obtain a substantially simpler proof for the decidability and PSPACE-membership of
the acyclic fragment of intersection of rational relations of [Barceló et al. 2013], which was
crucially used in [Lin and Barceló 2016] as a blackbox in their decidability proof of thestraight-line fragment.
(3) We define optimised translations from AFA emptiness to reachability over Boolean transition
systems (i.e. which are succinctly represented by Boolean formulae). We implemented ouralgorithm for string constraints in a new string solver called Sloth, and provide an extensive
experimental evaluation. Sloth is the first solver that can handle string constraints thatarise from HTML5 applications with sanitisation and implicit browser transductions. Our
experiments suggest that the translation to AFAs can circumvent the EXPSPACE worst-casecomplexity of the straight-line fragment in many practical cases.
An overview of the results. The main technical contribution of our paper is a new method for
exploiting alternating automata (AFA) as a succinct symbolic representation for representing
formulae in a complex string logic admitting concatenation and finite-state transductions. In
particular, the satisfiability problem for the string logic is reduced to AFA language emptiness, forwhich we exploit fast model checking algorithms. Compared to previous methods [Abdulla et al.
2014; Lin and Barceló 2016] that are based on nondeterministic automata (NFA) and transducers,
we show that AFA can incur at most a linear blowup for each string operation permitted in the
logic (i.e. concatenation, transducers, and regular constraints). While the product NFA representing
the intersection of the languages of two automata A1 and A2 would be of size O (|A1 | × |A2 |), thelanguage can be represented using an AFA of size |A1 | + |A2 | (e.g. see [Vardi 1995]). The difficult
cases are how to deal with concatenation and replace-all, which are our contributions to the paper.
More precisely, a constraint of the form x := y.z ∧ x ∈ L (where L is the language accepted by anautomaton A) was reduced in [Abdulla et al. 2014; Lin and Barceló 2016] to regular constraints ony and z by means of splitting A, which causes a cubic blow-up (since an “intermediate state” in A
has to be guessed, and for each state a product of two automata has to be constructed). Similarly,
taking the post-image R(L) of L under a relation R represented by a finite-state transducer T gives
us an automaton of size O (|T | × |A|). A naïve application of AFAs is not helpful for those cases,
since also projections on AFAs are computationally hard.
The key idea to overcome these difficulties is to avoid applying projections altogether, and instead
use the AFA to represent general k-ary rational relations (a.k.a. k-track finite-state transductions[Barceló et al. 2013; Berstel 1979; Sakarovitch 2009]). This is possible because we focus on formulae
without negation, so that the (implicit) existential quantifications for applications of transducers
can be placed outside the constraint. This means that our AFAs operate on alphabets that are
exponential in size (for k-ary relations, the alphabet is {ϵ, 0, 1}k ). To address this problem, we
introduce a succinct flavour of AFA with symbolically represented transitions. Our definition issimilar to the concept of alternating symbolic automata in [D’Antoni et al. 2016] with one difference.
While symbolic AFA take a transition q →ψ φ from a state q to a set of states satisfying a formula φ
if the input symbol satisfies a formula ψ , our succinct AFA can mix constraints on successor stateswith those on input symbols within a single transition formula (similarly to the symbolic transition
representation of deterministic automata in MONA [Klarlund et al. 2002], where sets of transitions

4

are represented as multi-terminal BDDs with states as terminal nodes). We show how automata
splitting can be achieved with at most linear blow-up.
The succinctness of our AFA representation of string formulae is not for free since AFA language
emptiness is a PSPACE-complete problem (in contrast to polynomial-time for NFA). However,modern model checking algorithms and heuristics can be harnessed to solve the emptiness problem.
In particular, we use a linear-time reduction to reachability in Boolean transition systems similar to[Cox and Leasure 2017; Wang et al. 2016], which can be solved by state of the art model checking
algorithms, such as IC3 [Bradley 2012], k-induction [Sheeran et al. 2000], or Craig interpolationbased methods [McMillan 2003], and tools like nuXmv [Cavada et al. 2014] or ABC [Brayton andMishchenko 2010].
An interesting by-product of our approach is an efficient decision procedure for the acyclic
fragment. The acyclic logic does not a priori allow concatenation, but is more liberal in the use oftransducer constraints (which can encode complex relations like string-length comparisons, andthe subsequence relation). In addition, such a logic is of interest in the investigation of complex
path-queries for graph databases [Barceló et al. 2013; Barceló et al. 2012], which has been pursued
independently of strings for verification. Our algorithm also yields an alternative and substantiallysimpler proof of PSPACE upper bound of the satisfiability problem of the logic.
We have implemented our AFA-based string solver as the tool Sloth, using the infrastructure
provided by the SMT solver Princess [Rümmer 2008], and applying the nuXmv [Cavada et al. 2014]
and ABC [Brayton and Mishchenko 2010] model checkers to analyse succinct AFAs. Sloth isa decision procedure for the discussed fragments of straight-line and acyclic string formulae, andis able to process SMT-LIB input with CVC4-style string operations, augmented with operations
str.replace, str.replaceall3 , and arbitrary transducers defined using sets of mutually recursivefunctions. Sloth is therefore extremely flexible at supporting intricate string operations, including
escape operations such as the ones discussed in Example 1.1. Experiments with string benchmarks
drawn from the literature, including problems with replace, replace-all, and general transducers,
show that Sloth can solve problems that are beyond the scope of existing solvers, while it iscompetitive with other solvers on problems with a simpler set of operations.
Organisation. We recall relevant notions from logic and automata theory in Section 2. In Section 3,
we define a general string constraint language and mention several important decidable restrictions.
In Section 4, we recall the notion of alternating finite-state automata and define a succinct variant
that plays a crucial role in our decision procedure. In Section 5, we provide a new algorithm
for solving the acyclic fragment of the intersection of rational relations using AFA. In Section 7,
we provide our efficient reduction from the straight-line fragment to the acyclic fragment that
exploits AFA constructions. To simplify the presentation of this reduction, we first introduce inSection 6 a syntactic sugar of the acyclic fragment called acyclic constraints with synchronisation
parameters. In Section 8, we provide our reduction from the AFT emptiness to reachability in a
Boolean transition system. Experimental results are presented in Section 9. Our tool Sloth can beobtained from https://github.com/uuverifiers/sloth/wiki. Finally, we conclude in Section 10. Missing
proofs can be found in the appendix.
2

PRELIMINARIES

Logic. Let B = {0, 1} be the set of Boolean values, and A a set of Boolean variables. We write FA
to denote the set of Boolean formulae over A. In this context, we will sometimes treat subsets A′ of
A as the corresponding truth assignments {s 7→ 1 | s ∈ A′ } ∪ {s 7→ 0 | s ∈ A \ A′ } and write, for
3 str.replaceall is the SMT-LIB syntax for the replace-all operation. On the other hand, str.replace represents theoperation of replacing the first occurrence of the given pattern. In case there is no such occurrence, the string stays intact.
5

instance, A′ |= φ for φ ∈ FA if the assignment satisfies φ. An atom is a Boolean variable; a literal iseither a atom or its negation. A formula is in disjunctive normal form (DNF) if it is a disjunctionof conjunctions of literals, and in negation normal form (NNF) if negation only occurs in frontof atoms. We denote the set of variables in a formula φ by var(φ). We use x̄ to denote sequences
x 1 , . . . , x n of length |x̄ | = n of propositional variables, and we write φ(x̄ ) to denote that x̄ are thevariables of φ. If we do not fix the order of the variables, we write φ(X ) for a formula with X being
its set of variables. For a variable vector x̄, we denote by {x̄ } the set of variables in the vector.
We say that φ is positive (negative) on an atom α ∈ A if α appears under an even (odd) numberof negations only. A formula that is positive (negative) on all its atoms is called positive (negative),
respectively. The constant formulae true and false are both positive and negative. We use FS+ andFS− to denote the sets of all positive and negative Boolean formulae over S, respectively.
Given a formula φ, we write φH to denote a formula obtained by replacing (1) every conjunction
by a disjunction and vice versa and (2) every occurrence of true by false and vice versa. Notethat xH = x, which means that φH is not the same as the negation of φ.
Strings and languages. Fix a finite alphabet Σ. Elements in Σ∗ are interchangeably called words
or strings, where the empty word is denoted by ϵ. The concatenation of strings u, v is denoted byu ◦ v, occasionally just by uv to avoid notational clutter. We denote by |w | the lenght of a wordw ∈ Σ∗ . For any word w = a 1 . . . an , n ≥ 1, and any index 1 ≤ i ≤ n, we denote by w[i] theletter ai . A language is a subset of Σ∗ . The concatenation of two languages L, L ′ is the language
L ◦ L ′ = {w ◦ w ′ | w ∈ L ∧ w ′ ∈ L ′ }, and the iteration L∗ of a language L is the smallest language
closed under ◦ and containing L and ϵ.
Regular languages and rational relations. A regular language over a finite alphabet Σ is a subset ofΣ∗ that can be built by a finite number of applications of the operations of concatenation, iteration,and union from the languages {ϵ } and {a}, a ∈ Σ. An n-ary rational relation R over Σ is a subset of(Σ∗ ) n that can be obtained from a regular language L over the alphabet of n-tuples (Σ ∪ {ϵ }) n as
follows. Include (w 1 , . . . , w n ) in R iff for some (a 11 , . . . , an1 ), . . . , (ak1 , . . . , akn ) ∈ L, w i = a 1 ◦ · · · ◦ ak
for all 1 ≤ i ≤ n. Here, ◦ is a concatenation over the alphabet Σ, and k denotes the length of thewords w i . In practice, regular languages and rational relations can be represented using various
flavours of finite-state automata, which are discussed in detail in Section 4.
3

STRING CONSTRAINTS

We start by recalling a general string constraint language from [Lin and Barceló 2016] that supports
concatenations, finite-state transducers, and regular expression matching. We will subsequently
state decidable fragments of the language for which we design our decision procedure.
3.1

String Language

We assume a vocabulary of countably many string variables x, y, z, . . . ranging over Σ∗ . A string
formula over Σ is a Boolean combination φ of word equations x = t whose right-hand side t might
contain the concatenation operator, regular constraints P (x ), and rational constraints R (x̄ ):φ ::= x = t | P (x ) | R (x̄ ) | φ ∧ φ | φ ∨ φ | ¬φ,t ::= x | a | t ◦ t .

In the grammar, x ranges over string variables, x̄ over vectors of string variables, and a ∈ Σ overletters. R ⊆ (Σ∗ ) n is assumed to be an n-ary rational relation on words of Σ∗ , and P ⊆ Σ∗ is a regular
language. We will represent regular languages and rational relations by succinct automata andtransducers denoted as R and A, respectively. The automata and transducers will be formalized in
Section 4. When the transducer R or automaton A representing a rational relation R or regular
language P is known, we write R (x̄ ) or A (x̄ ) instead of R(x̄ ) or P (x̄ ) in the formulae, respectively.
6

A formula φ is interpreted over an assignment ι : var(φ) → Σ∗ of its variables to strings overΣ∗ . It satisfies φ, written ι |= φ, iff the constraint φ becomes true under the substitution of eachvariable x by ι(x ). We formalise the satisfaction relation for word equations, rational constraints,
and regular constraints, assuming the standard meaning of Boolean connectives:(1) ι satisfies the equation x = t if ι(x ) = ι(t ), extending ι to terms by setting ι(a) = a andι(t 1 ◦ t 2 ) = ι(t 1 ) ◦ ι(t 2 ).
(2) ι satisfies the rational constraint R (x 1 , . . . , x n ) iff (ι(x 1 ), . . . , ι(x n )) belongs to R.
(3) ι satisfies the regular constraint P (x ), for P a regular language, if and only if ι(x ) ∈ P.
A satisfying assignment for φ is also called a solution for φ. If φ has a solution, it is satisfiable.
The unrestricted string logic is undecidable, e.g., one can easily encode Post Correspondence
Problem (PCP) as the problem of checking satisfiability of the constraint R (x, x ), for some rationaltransducer R [Morvan 2000]. We therefore concentrate on practical decidable fragments.
3.2

Decidable Fragments

Our approach to deciding string formulae is based on two major insights. The first insight is thatalternating automata can be used to efficiently decide positive Boolean combinations of rational
constraints. This yields an algorithm for deciding (an extension of) the acyclic fragment of [Barceló
et al. 2013]. The minimalistic definition of acyclic logic restricts rational constraints and does notallow word equations (in Section 5.1 a limited form of equations and arithmetic constraints overlengths will be shown to be encodable in the logic). Our definition of the acyclic logic AC below
generalises that of [Barceló et al. 2013] by allowing k-ary rational constraints instead of binary.
Definition 3.1 (Acyclic formulae). Particularly, we say that a string formula φ is acyclic if it does
not contain word equations, rational constraints R (x 1 , . . . , x n ) only appear positively and theirvariables x 1 , . . . , x n are pairwise distinct, and for every sub-formula ψ ∧ ψ ′ at a positive position ofφ (and also every ψ ∨ ψ ′ at a negative position) it is the case that |free(ψ ) ∩ free(ψ ′ )| ≤ 1, i.e., ψand ψ ′ have at most one variable in common. We denote by AC the set of all acyclic formulae.
The second main insight we build on is that alternation allows a very efficient encoding of
concatenation into rational constraints and automata (though only equisatisfiable, not equivalent).
Efficient reasoning about concatenation combined with rational relations is the main selling pointof our work from the practical perspective—this is what is most needed and was so far missing
in applications like security analysis of web-applications. We follow the approach from [Linand Barceló 2016] which defines so called straight-line conjunctions. Straight-line conjunctions
essentially correspond to sequences of program assignments in the single static assignment form,
possibly interleaved with assertions of regular properties. An equation x = y1 ◦· · ·◦yn is understoodas an assignment to a program variable x. A rational constraint R (x, y) may be interpreted as an
assignment to x as well, in which case we write it as x = R (y) (though despite the notation, R is
not required to represent a function, it can still mean any rational relation).
Definition 3.2 (Straight-line conjunction). A conjunction of string constraints is then defined toVbe straight-line if it can be written as ψ ∧ m
i=1 x i = Pi where ψ is a conjunction of regular andnegated regular constraints and each Pi is either of the form y1 ◦ · · · ◦ yn , or R(y) and, importantly,
Pi cannot contain variables x i , . . . , xm . We denote by SL the set of all straight-line conjunctions.
Example 3.3. The program snippet in Example 1.1 would be expressed as x = R 1 (name) ∧ y =R 2 (x ) ∧ z = w 1 ◦ y ◦ w 2 ◦ x ◦ w 3 ∧ u = R 3 (z). The transducers Ri correspond to the string
operations at the respective lines: R 1 is the htmlEscape, R 2 is the escapeString, and R 3 is theimplicit transduction within innerHTML. Line 3 is translated into a conjunction of the concatenationand the third rational constraint encoding the implicit string operation at the assignment to7

innerHTML. In the concatenation, w 1 , w 2 , w 3 are words that correspond to the three constantstrings concatenated with x and y on line 3. To test vulnerability, a regular constraint A(u)encoding the pattern e1 is added as a conjunct.
The fragment of straight-line conjunctions can be straightforwardly extended to disjunctive
formulae. We say that a string formula is straight-line if every clause in its DNF is straightline. A decision procedure for straight-line conjunctions immediately extends to straight-line
formulae: instantiate the DPLL(T) framework [Nieuwenhuis et al. 2004] with a solver for straightline conjunctions.
The straight-line and acyclic fragments are clearly syntactically incomparable: AC does not haveequations, SL restricts more strictly combinations of rational relations and allows only binary
ones. Regarding expressive power, SL can express properties which AC cannot: the straight-line
constraint x = yy cannot be expressed by any acyclic formula. On the other hand, whether or not
AC formulae can be expressed in SL is not clear. Every AC formula can be expressed by a single n-ary
acyclic rational constraint (c.f. Section 5), hence acyclic formulae and acyclic rational constraints
are of the same power. It is not clear however whether straight-line formulae, which can use only
binary rational constraints, can express arbitrary n-ary acyclic rational constraint.
4

SUCCINCT ALTERNATING AUTOMATA AND TRANSDUCERS

We introduce a succinct form of alternating automata and transducers that operate over bit vectors,i.e., functions b : V → B where V is a finite, totally ordered set of bit variables. This is a variant of
the recent automata model in [D’Antoni et al. 2016] that is tailored to our problem. Bit vectors canof course be described by strings over B, conjunctions of literals over V , or sets of those elementsv ∈ V such that b (v) = 1. In what follows, we will use all of these representations interchangeably.
Referring to the last mentioned possibility, we denote the set of all bit vectors over V by P (V ).
An obvious advantage of this approach is that encoding symbols of large alphabets, such as UTF,
by bit vectors allows one to succinctly represent sets of such symbols using Boolean formulae. In
particular, symbols of an alphabet of size 2k can be encoded by bit vectors of size k (or, alternatively,
as Boolean formulae over k Boolean variables). We use this fact when encoding transitions of ouralternating automata.
Example 4.1. To illustrate the encoding, assume the alphabet Σ = {a, b, c, d } consisting of symbols
a, b, c, and d. We can deal with this alphabet by using the set V = {v 0 , v 1 } and representing, e.g., aas ¬v 1 ∧ ¬v 0 , b as ¬v 1 ∧ v 0 , c as v 1 ∧ ¬v 0 , and d as v 1 ∧ v 0 . This is, a, b, c, and d are encoded as the
bit vectors 00, 01, 10, and 11 (for the ordering v 0 < v 1 ), or the sets ∅, {v 0 }, {v 1 }, {v 0 , v 1 }, respectively.
The set of symbols {c, d } can then be encoded simply by the formula v 1 .
□4.1

Succinct Alternating Finite Automata

A succinct alternating finite automaton (AFA) over Boolean variables V is a tuple A = (V , Q, ∆, I , F )where Q is a finite set of states, the transition function ∆ : Q → FV ∪Q assigns to every state a Boolean
formula over Boolean variables and states that is positive on states, I ∈ FQ+ is a positive initial
formula, and F ∈ FQ− is a negative final formula. Let w = b1 . . . bm , m ≥ 0, be a word where each bi ,1 ≤ i ≤ m, is a bit vector encoding the i-th letter of w. A run of the AFA A over w is a sequenceρ = ρ 0b1 ρ 1 . . . bm ρm where bi ∈ P (V ) for every 1 ≤ i ≤ m, ρ i ⊆ Q for every 0 ≤ i ≤ m, andVbi ∪ ρ i |= q ∈ρ i −1 ∆(q) for every 1 ≤ i ≤ m. The run is accepting if ρ 0 |= I and ρm |= F , in whichcase the word is accepted. The language of A is the set L(A) of accepted words.
Notice that instead of the more usual definition of ∆, which would assign a positive Boolean
formula over Q to every pair from Q × P (V ) or to a pair Q × FV as in [D’Antoni et al. 2016], we
let ∆ assign to states formulae that talk about both target states and Boolean input variables. This8

is closer to the encoding of the transition function as used in MONA [Klarlund et al. 2002]. It
allows for additional succinctness and also for a more natural translation of the language emptinessproblem into a model checking problem (cf. Section 8).4 Moreover, compared with the usual AFA
definition, we do not have just a single initial state and a single set of accepting states, but we
use initial and final formulae. As will become clear in Section 5, this approach allows us to easilytranslate the considered formulae into AFAs in an inductive way.
Note that standard nondeterministic finite automata (NFAs), working over bit vectors, can beobtained as a special case of our AFAs as follows. An AFA A = (V , Q, ∆, I , F ) is an NFA iff (1) I isW
Vof the form q ∈Q ′ q for some Q ′ ⊆ Q, (2) F is of the form q ∈Q ′′ ¬q for some Q ′′ ⊆ Q, and (3) forW
every q ∈ Q, ∆(q) is of the form 1≤i ≤m φ i (V ) ∧ qi where m ≥ 0 and, for all 1 ≤ i ≤ m, φ i (V ) is
a formula over the input bit variables and qi ∈ Q.
Example 4.2. To illustrate our notion of AFAs, we give an example of an AFA A over thealphabet Σ = {a, b, c, d } from Example 4.1 that accepts the language {w ∈ Σ∗ | |w | mod 35 = 0 ∧∀i∃j : (1 ≤ i ≤ |w | ∧ w[i] ∈ {a, b}) → (i < j ≤ |w | ∧ w[j] ∈ {c, d })}, i.e., the length of
the words is a multiple of 35, and every letter a or b is eventually followed by a letter c or d.
In particular, we let A = ({v 0 , v 1 }, {q 0 , . . . , q 4 , p0 , . . . , p6 , r 1 , r 2 }}, ∆, I , F ) where I = q 0 ∧ p0 , F =¬q 1 ∧ . . . ∧ ¬q 4 ∧ ¬p1 ∧ . . . ∧ ¬p6 ∧ ¬r 1 (i.e., the accepting states are q 0 , p0 , and r 2 ), and ∆ is defined
as follows:• ∀0 ≤ i < 5 : ∆(qi ) = (¬v 1 ∧ q (i+1) mod 5 ∧ r 1 ) ∨ (v 1 ∧ q (i+1) mod 5 ),• ∀0 ≤ i < 7 : ∆(pi ) = p (i+1) mod 7 ,• ∆(r 1 ) = (v 1 ∧ r 2 ) ∨ (¬v 1 ∧ r 1 ) and ∆(r 2 ) = r 2 .
Intuitively, the q states check divisibility by 5. Moreover, whenever, they encounter an a or b symbol(encoded succinctly as checking ¬v 1 in the AFA), they spawn a run through the r states, whichchecks that eventually a c or d symbol appears. The p states then check divisibility by 7. The desired
language is accepted due to the requirement that all these runs must be synchronized. Note that
encoding the language using an NFA would require quadratically more states since an explicit
product of all the branches would have to be done.
□
The additional succinctness of AFA does not influence the computational complexity of theemptiness check compared to the standard variant of alternating automata.
Lemma 4.3. The problem of language emptiness of AFA is PSPACE-complete.
The lemma is witnessed by a linear-space transformation of the problem of emptiness of an AFA
language to the PSPACE-complete problem of reachability in a Boolean transition system. Thistransformation is shown in Section 8.
4.2

Boolean Operations on AFAs

From the standard Boolean operations over AFAs, we will mainly need conjunction and disjunctionin this paper. These operations can be implemented in linear space and time in a way analogous to[D’Antoni et al. 2016], slightly adapted for our notion of initial/final formulae, as follows. Given
two AFAs A = (V , Q, ∆, I, F ) and A ′ = (V , Q ′, ∆ ′, I ′, F ′ ) with Q ∩ Q ′ = ∅, the automaton accepting
the union of their languages can be constructed as A ∪ A ′ = (V , Q ∪ Q ′, ∆ ∪ ∆ ′, I ∨ I ′, F ∧ F ′ ),and the automaton accepting the intersection of their languages can be constructed as A ∩ A ′ =(V , Q ∪ Q ′, ∆ ∪ ∆ ′, I ∧ I ′, F ∧ F ′ ). Seeing correctness of the construction of A ∩ A ′ is immediate.
4 [D’Antoni et al. 2016] also mentions an implementation of symbolic AFAs that uses MONA-like BDDs and is technicallyclose to our AFAs.

9

Indeed, the initial condition enforces that the two AFAs run in parallel, disjointness of their statespaces prevents them from influencing one another, and the final condition defines their parallelruns as accepting iff both of the runs accept. To see correctness of the construction of A ∪ A ′,it is enough to consider that one of the automata can be started with the empty set of statesV(corresponding to the formula q ∈Q ¬q for A and likewise for A ′). This is possible since only oneof the initial formulae I and I ′ needs to be satisfied. The automaton that was started with the empty
set of states will stay with the empty set of states throughout the entire run and thus triviallysatisfy the (negative) final formula.
Example 4.4. Note that the AFA in Example 4.2 can be viewed as obtained by conjunction of two
AFAs: one consisting of the q and r states and the second of the p states.
□
To complement an AFA A = (V , Q, ∆, I , F ), we first transform the automaton into a form
corresponding to the symbolic AFA of [D’Antoni et al. 2016] and then use their complementation
procedure. More precisely, the transformation to the symbolic AFA form requires two steps:• The first step simplifies the final condition. The final formula F is converted into DNF, yielding
a formula F 1 ∨ . . . ∨ Fk , k ≥ 1, where each Fi , 1 ≤ i ≤ k, is a conjunction of negative literals
over Q. The AFA A is then transformed into a union of AFAs Ai = (V , Q, ∆, I, Fi ), 1 ≤ i ≤ k,where each Ai is a copy of A except that it uses one of the disjuncts Fi of the DNF form of
the original final formula F as its final formula. Each resulting AFAs hence have a purely
conjunctive final condition that corresponds a set of final states of [D’Antoni et al. 2016].
• The second step simplifies the structure of the transitions. For every q ∈ Q, the transition
formula ∆(q) is transformed into a disjunction of formulae of the form (φ 1 (V ) ∧ψ 1 (Q )) ∨ . . . ∨(φm (V ) ∧ ψm (Q )) where the φ i (V ) formulae, called input formulae below, speak about input
bit variables only, while the ψi (Q ) formulae, called target formulae below, speak exclusively
about the target states, for 1 ≤ i ≤ m. For this transformation, a slight modification oftransforming a formula into DNF can be used.
The complementation procedure of [D’Antoni et al. 2016] then proceeds in two steps: thenormalisation and the complementation itself. We sketch them below:• For every q ∈ Q, normalisation transforms the transition formula ∆(q) = (φ 1 (V ) ∧ ψ 1 (Q )) ∨. . . ∨ (φm (V ) ∧ ψm (Q )) so that every two distinct input formulae φ(V ) and φ ′ (V ) of theresulting formula describe disjoint sets of bit vectors, i.e., ¬(φ(V ) ∧ φ ′ (V )) holds. To achieve
this (without trying to optimize the algorithm as in [D’Antoni et al. 2016]), one can consider
generating all Boolean combinations of the original φ(V ) formulae, conjoining each of themwith the disjunction of those state formulae whose input formulae are taken positively in theW
VVW
given case. More precisely, one can take I ⊆ {1, ...,m } ( i ∈I φ i ))∧( i ∈ {1, ...,m }\I ¬φ i ))∧ i ∈I ψi .
• Finally, to complement the AFAs normalized in the above way, one proceeds as follows:(1) The initial formula I is replaced by H
I . (2) For every q ∈ Q and every disjunct φ(V ) ∧ ψ (Q )of the transition formula ∆(q), the target formula ψ (Q ) is replaced by ψH(Q ). (3) The finalVV
formula of the form q ∈Q ′ ¬q, Q ′ ⊆ Q, is transformed to the formula q ∈Q \Q ′ ¬q, and false
is swapped for true and vice versa.
Clearly, the complementation contains three sources of exponential blow-up: (1) the simplificationof the final condition, (2) the simplification of transitions and (3) the normalization of transitions.
Note, however, that, in this paper, we will apply complementation exclusively on AFAs obtained
by Boolean operations from NFAs derived from regular expressions. Such AFAs already have thesimple final conditions, and so the first source of exponential blow-up does not apply. The second
and the third source of exponential complexity can manifest themselves but note that it does not10

show up in the number of states. Finally, note that if we used AFAs with explicit alphabets, thesecond and the third problem would disappear (but then the AFAs would usually be bigger anyway).

4.3

Succinct Alternating Finite Transducers

In our alternating finite transducers, we will need to use epsilon symbols representing the empty
word. Moreover, as we will explain later, in order to avoid some undesirable synchronization
when composing the transducers, we will need more such symbols—differing just syntactically.
Technically, we will encode the epsilon symbols using a set of epsilon bit variables E, containing one
new bit variable for each epsilon symbol. We will draw the epsilon bit variables from a countably
infinite set E. We will also assume that when one of these bits is set, other bits are not important.
Let W be a finite, totally ordered set of bit variables, which we can split to the set of input
bit variables V (W ) = W \ E and the set of epsilon bit variables E(W ) = W ∩ E. Given a word
w = b1 . . . bm ∈ P (W ) ∗ , m ≥ 0, we denote by ⟩w⟨ the word that arises from w by erasing
all those bi , 1 ≤ i ≤ m, in which some epsilon bit variable is set, i.e., bi ∩ E , ∅. Further,let k ≥ 1, and let W ⟨k⟩ = W × [k], assuming it to be ordered in the lexicographic way. The
indexing of the bit variables will be used to express the track on which they are read. Finally,
given a word w = b1 . . . bm ∈ P (W ⟨k⟩) ∗ , m ≥ 0, we denote by w ↓i , 1 ≤ i ≤ k, the word
′ ∈ P (W ) ∗ that arises from w by keeping the contents of the i-th track (without the index i)b1′ . . . bm
only, i.e., b j′ × {i} = b j ∩ (W × {i}) for 1 ≤ j ≤ m.
A k-track succinct alternating finite transducer (AFT) over W is syntactically an alternating
automaton R = (W ⟨k⟩, Q, ∆, I, F ), k ≥ 1. Let V = V (W ). The relation Rel(R) ⊆ (P (V ) ∗ ) k recognised
by R contains a k-tuple of words (x 1 , . . . , x k ) over P (V ) iff there is a word w ∈ L(R) such thatx i = ⟩w↓i ⟨ for each 1 ≤ i ≤ k.
Below, we will sometimes say that the word w encodes the k-tuple of words (x 1 , . . . , x k ). Moreover, for simplicity, instead of saying that R has a run over w that encodes (x 1 , . . . , x k ), we will
sometimes directly say that R has a run over (x 1 , . . . , x k ) or that R accepts (x 1 , . . . , x k ).
Finally, note that classical nondeterministic finite transducers (NFTs) are a special case of our
AFTs that can be defined by a similar restriction as the one used when restricting AFAs to NFAs.
In particular, the first track (with letters indexed with 1) can be seen as the input track, and thesecond track (with letters indexed with 2) can be seen as the output track. AFTs as well as NFTs
recognize the class of rational relations [Barceló et al. 2013; Berstel 1979; Sakarovitch 2009].

Example 4.5. We now give a simple example of an AFT that implements escaping of every
apostrophe by a backlash in the UTF-8 encoding. Intuitively, the AFT will transform an input stringx'xx to the string x\'xx, i.e., the relation it represents will contain the couple (x'xx,x\'xx). All
the symbols should, however, be encoded in UTF-8. In this encoding, the apostrophe has the binary
code 00100111, and the backlash has the code 00101010. We will work with the set of bit variables
V8 = {v 0 , . . . , v 7 } and a single epsilon bit variable e. We will superscript the bit variables by the
track on which they are read (hence, e.g., v 12 is the same as (v 1 , 2), i.e., v 1 is read on the second
track). Let api = v 0i ∧ v 1i ∧ v 2i ∧ ¬v 3i ∧ ¬v 4i ∧ v 5i ∧ ¬v 6i ∧ ¬v 7i ∧ ¬e i represent an apostrophe readon the i-th track. Next, let bci = ¬v 0i ∧ v 1i ∧ ¬v 2i ∧ v 3i ∧ ¬v 4i ∧ v 5i ∧ ¬v 6i ∧ ¬v 7i ∧ ¬e i representVa backlash read on the i-th track. Finally, let eqi, j = e i ↔ e j ∧ 0≤k <8 vki ↔ vkj denote that thesame symbol is read on the i-th and j-th track. The AFT that implements the described escaping canbe constructed as follows: R = ((V8 ∪ {e})⟨2⟩, {q 0 , q 1 }, ∆, q 0 , ¬q 1 ) where the transition formulae aredefined by ∆(q 0 ) = (¬ap1 ∧ eq1,2 ∧ q 0 ) ∨ (ap1 ∧ bc2 ∧ q 1 ) and ∆(q 1 ) = e 1 ∧ ap2 ∧ q 0 .
□
11

5

DECIDING ACYCLIC FORMULAE

Our decision procedure for AC formulae is based on translating them into AFTs. For simplicity, we
assume that the formula is negation free (after transforming to NNF, negation at regular constraints
can be eliminated by AFA complementation). Notice that with no negations, the restriction AC
puts on disjunctions never applies. We also assume that the formula contains rational constraints
only (regular constraint can be understood as unary rational constraints).
Our algorithm then transforms a formula φ(x̄ ) into a rational constraint Rφ (x̄ ) inductively on
the structure of φ. As the base case, we get rational constraints R (x̄ ), which are already represented
as AFTs, and regular constraints A (x ), already represented by AFAs. Boolean operations overregular constraints can be treated using the corresponding Boolean operations over AFAs describedin Section 4.2. The resulting AFAs can then be viewed as rational constraints with one variable(and hence as a single-track AFT).
Once constraints Rφ (x̄ ) and Rψ (ȳ) are available, the induction step translates formulae Rφ (x̄ ) ∧Rψ (ȳ) and Rφ (x̄ ) ∨ Rψ (ȳ) to constraints Rφ∧ψ (z̄) and Rφ∨ψ (z̄), respectively. To be able to describe
this step in detail, let Rφ = ((V ∪ Eφ )⟨|x̄ |⟩, Q φ , ∆φ , Iφ , Fφ ) and Rψ = ((V ∪ Eψ )⟨|ȳ|⟩, Qψ , ∆ψ , Iψ , Fψ )such that w.l.o.g. Q φ ∩ Qψ = ∅ and Eφ ∩ Eψ = ∅.
Translation of conjunctions to AFTs. The construction of Rφ∧ψ has three steps:(1) Alignment of tracks that ensures that distinct variables are assigned different tracks andthat the transducers agree on the track used for the shared variable.
(2) Saturation by ϵ-self loops allowing the AFTs to synchronize whenever one of them makes
an ϵ move on the shared track.
(3) Conjunction on the resulting AFTs viewing them as AFAs.
Alignment of tracks. Given constraints Rφ (x̄ ) and Rψ (ȳ), the goal of the alignment of tracks is
to assign distinct tracks to distinct variables of x̄ and ȳ, and to assign the same track in both of thetransducers to the shared variable—if there is one (recall that, by acyclicity, x̄ and ȳ do not containrepeating variables and share at most one common variable). This is implemented by choosing
a vector z̄ that consists of exactly one occurrence of every variable from x̄ and ȳ, i.e., {z̄} = {x̄ } ∪ {ȳ},and by subsequently re-indexing the bit vector variables in the transition relations. Particularly, in∆φ , every indexed bit vector variable v i (including epsilon bit variables) is replaced by v j with jbeing the position of x i in z̄, and analogously in ∆ψ , every indexed bit variable v i is replaced by v jwith j being the position of yi in z̄. Both AFTs are then considered to have |z̄| tracks.
Saturation by ϵ-self loops. This step is needed if x̄ and ȳ share a variable, i.e., {x̄ }∩{ȳ} , ∅. The two
input transducers then have to synchronise on reading its symbols. However, it may happen that,at some point, one of them will want to read from the non-shared tracks exclusively, performing an
ϵ transition on the shared track. Since reading of the non-shared tracks can be ignored by the othertransducer, it should be allowed to perform an ϵ move on all of its tracks. However, that needs
not be allowed by its transition function. To compensate for this, we will saturate the transition
function by ϵ-self loops performed on all tracks. Unfortunately, there is one additional problem
with this step: If the added ϵ transitions were based on the same epsilon bit variables as thosealready used in the given AFT, they could enable some additional synchronization within the given
AFT, thus allowing it to accept some more tuples of words. We give an example of this problem
below (Example 5.2). To resolve the problem, we assume that the two AFTs being conjuncted use
different epsilon bit variables (more of such variables can be used due the AFTs can be a result of
several previous conjunctions). Formally, for any choice σ , σ ′ ∈ {φ,ψ } such that σ , σ ′, and forWVevery state q ∈ Q σ , the transition formula ∆σ (q) is replaced by ∆σ (q) ∨ (q ∧ e ∈E σ ′ i ∈[|z̄ |] e i ).
12

Conjunction of AFTs viewed as AFAs. In the last step, the input AFTs with aligned tracks and saturated by ϵ-self loops are conjoined using the automata intersection construction from Section 4.2.
Lemma 5.1. Let Rφ′ and Rψ′ be the AFTs obtained from the input AFTs Rφ and Rψ by track alignmentand ϵ-self-loop saturation, and let Rφ∧ψ = Rφ′ ∩ Rψ′ . Then, Rφ∧ψ (z̄) is equivalent to Rφ (x̄ ) ∧ Rψ (ȳ).
To see that the lemma holds, note that both Rφ′ and Rψ′ have the same number of tracks—namely,|z̄|. This number can be bigger than the original number of tracks (|x̄ | or |ȳ|, resp.), but the AFTs
still represent the same relations over the original tracks (the added tracks are unconstrained).
The ϵ-self loop saturation does not alter the represented relations either as the added transitions
represent empty words across all tracks only, and, moreover, they cannot synchronize with theoriginal transitions, unblocking some originally blocked runs. Finally, due to the saturation, the two
AFTs cannot block each other by an epsilon move on the shared track available in one of them only.5
Example 5.2. We now provide an example illustrating the conjunction of AFTs, including theneed to saturate the AFTs by ϵ-self loops with different ϵ symbols. We will assume working with
the input alphabet Σ = {a, b} encoded using a single input bit variable v 0 : let a correspond to ¬v 0
and b to v 0 . Moreover, we will use two epsilon bit variables, namely, e 1 and e 2 . We consider thefollowing two simple AFTs, each with two tracks:• R 1 = ({v 0 , e 1 }⟨2⟩, {q 0 , q 1 , q 2 }, ∆1 , q 0 , ¬q 0 ∧¬q 2 ) with ∆1 (q 0 ) = (a 1 ∧b 2 ∧q 1 ) ∨ (a 1 ∧a 2 ∧q 1 ∧q 2 ),
∆1 (q 1 ) = false, and ∆1 (q 2 ) = e 11 ∧ q 1 . Note that Rel(R 1 ) = {(a, b)} since the run that starts
with a 1 ∧ a 2 gets stuck in one of its branches, namely the one that goes to q 2 . This is because
we require branches of a single run of an AFT to synchronize even on epsilon bit variables,
and the transition from q 2 cannot synchronize with any move from q 1 .
• R 2 = ({v 0 , e 2 }⟨2⟩, {p0 , p1 , p2 }, ∆2 , p0 , ¬p0 ∧ ¬p1 ) such that ∆2 (p0 ) = (a 1 ∧ b 2 ∧ p1 ), ∆2 (p1 ) =e 21 ∧ b 2 ∧ p2 , and ∆2 (p2 ) = false. Clearly, Rel(R 2 ) = {(a, bb)}.
Let Q i , Ii , Fi denote the set of states, initial constraint, and final constraint of Ri , i ∈ {1, 2},
respectively. Assume that we want to construct an AFT for the constraint R 1 (x, y) ∧ R 2 (x, z).
This constraint represents the ternary relation {(a, b, bb)}. It can be seen that if we apply theabove described construction for intersection of AFTs to R 1′ and R 2′ , where R 1′ = R 1 and R 2′
is the same as R 2 up to all symbols from track to 2 are moved to track 3, we will get an AFT
R = ({v 0 , e 1 , e 2 }⟨3⟩, Q 1 ∪ Q 2 , ∆, I 1 ∧ I 2 , F 1 ∧ F 2 ) representing exactly this relation. We will not list
here the entire ∆ but let us note the below:• ∆ will contain the following transition obtained by ϵ-self-loop saturation of R 1 : ∆(q 1 ) =(e 21 ∧ e 22 ∧ q 1 ). This will allow R to synchronize its run through q 1 with its run from p1 to p2 .
Without the saturation, this would not be possible, and Rel(R) would be empty.
• On the other hand, if a single epsilon bit variable e was used in both AFTs as well as intheir saturation, the saturated ∆1 would include the transition ∆1 (q 1 ) = (e 1 ∧ e 2 ∧ q 1 ). Thistransition could synchronize with the transition ∆1 (q 2 ) = e 1 ∧q 1 , and the relation represented
by the saturated R 1 would grow to Rel(R 1 ) = {(a, b), (a, a)}. The result of the intersection
would then (wrongly) represent the relation {(a, b, bb), (a, a, bb)}.
□
Translation of disjunctions to AFTs. The construction of an AFT for a disjunction of formulae
is slightly simpler. The alignment of variables is immediately followed by an application of the
AFA disjunction construction. That is, the AFT Rφ∨ψ is constructed simply as Rφ′ ∪ Rψ′ from theconstraints Rφ′ (z̄) and Rψ′ (z̄) produced by the alignment of the vectors of variables x̄ and ȳ in
5 Note that the same approach cannot be used for AFTs sharing more than one track. Indeed, by intersecting two general

rational relations, one needs not obtain a rational relation.

13

Rφ (x̄ ) and Rψ (ȳ). The construction of Rφ′ and Rψ′ does not require the saturation by ϵ-self loops
because the two transducers do not need to synchronise on reading shared variables. The vectors x̄
and ȳ are allowed to share any number of variables.
Theorem 5.3. Every acyclic formula φ(x̄ ) can be transformed into an equisatisfiable rational
constraint R (x̄ ) represented by an AFT R. The transformation can be done in polynomial time unlessφ contains a negated regular constraint represented by a non-normalized succinct NFA.
Corollary 5.4. Checking satisfiability of acyclic formulae is in PSPACE unless the formulae containa negated regular constraint represented by a non-normalized succinct NFA.
PSPACE membership of satisfiability of acyclic formulae with binary rational constraints (without
negations of regular constraints and without considering succinct alphabet encoding) is provenalready in [Barceló et al. 2013]. Apart from extending the result to k-ary rational constraints, we
obtain a simpler proof as a corollary of Theorem 5.3, avoiding a need to use the highly intricate
polynomial-space procedure based on the Savitch´s trick used in [Barceló et al. 2013]. Not considering the problem of negating regular constraints, our PSPACE algorithm would first constructa linear-size AFT for the input φ. We can then use the fact that the standard PSPACE algorithm forchecking emptiness of AFAs/AFTs easily generalises to succinct AFAs/AFTs. This is proved by ourlinear-space reduction of emptiness of the language of succinct AFAs to reachability in Booleantransition systems, presented in Section 8. Reachability in Boolean transition systems is known to
be PSPACE-complete.
5.1

Decidable Extensions of AC

The relatively liberal condition that AC puts on rational constraints allow us to easily extend
AC with other features, without having to change the decision procedure. Namely, we can add
Presburger constraints about word length, as well as word equations, as long as overall acyclicity
of a formula is preserved. Length constraints can be added in the general form φ Pres (|x 1 |, . . . , |x k |),where φ Pres is a Presburger formula.
Definition 5.5 (Extended acyclic formulae). A string formula φ augmented with length constraints
φ Pres (|x 1 |, . . . , |x k |) is extended acyclic if every word equation or rational constraint contains eachvariable at most once, rational constraints R (x 1 , . . . , x n ) only appear at positive positions, and forevery sub-formula ψ ∧ ψ ′ at a positive position of φ (and also every ψ ∨ ψ ′ at a negative position)
it is the case that |free(ψ ) ∩ free(ψ ′ )| ≤ 1, i.e., ψ and ψ ′ have at most one variable in common.
Any extended AC formula φ can be turned into a standard AC formula by translating word
equations and length constraints to rational constraints. Notice that, although quite powerful,extended AC still cannot express SL formulae such as x = yy, and does not cover practical properties
such as, e.g., those in Example 3.3 (where two conjuncts contain both x and y).
Word equations to rational constraints. For simplicity, assume that equations do not containletters a ∈ Σ. This can be achieved by replacing every occurrence of a constraint b by a fresh variable
constrained by the regular language {b}. An equation x = x 1 ◦ · · · ◦ x n without multiple occurrencesof any variables is translated to a rational constraint R (x, x 1 , . . . , x n ) with R = (W ⟨n + 1⟩, Q ={q 0 , . . . , qn }, ∆, I = q 0 , F = qn ). The transitions for i ∈ [n] are^^∆(qi−1 ) = (qi−1 ∨ qi ) ∧ej ∧(v i ↔ v 0 ).
j ∈[n]\{i }v ∈W ⟨n+1⟩

and ∆(qn ) = false. That is, the symbol on the first track is copied to the ith track while all theother tracks read ϵ. Negated word equations can be translated to AFTs in a similar way.
14

Length constraints to rational constraints. The translation of length constraints to rational constraints is similarly straightforward. Suppose an extended AC formula contains a length constraint φ Pres (|x 1 |, . . . , |x k |), where φ Pres is a Presburger formula over k variables y1 , . . . , yk ranging
over natural numbers. It is a classical result that the solution space of φ Pres forms a semi-linear
set [Ginsburg and Spanier 1966], i.e., can be represented as a finite union of linear sets L j =Pkk{ȳ0 + mi=1 λ i ȳi | λ 1 , . . . , λm ∈ N} ⊆ N with ȳ 0 , . . . ȳm ∈ N . Every linear set L j can directly be translated to a succinct k-track AFT recognising the relation {(x 1 , . . . , x k ) ∈ (Σ∗ ) k | (|x 1 |, . . . , |x k |) ∈ L j },and the union of AFTs be constructed as shown in Section 4.2, resulting in an AFT Rφ Pres (x 1 , . . . , x k )that is equivalent to φ Pres (|x 1 |, . . . , |x k |).
6

RATIONAL CONSTRAINTS WITH SYNCHRONISATION PARAMETERS

In order to simplify the decision procedure for SL, which we will present in Section 7, we introduce
an enriched syntax of rational constraints. We will then extend the AC decision procedure from
Section 5 to the new type of constraints such that it can later be used as a subroutine in our decision
procedure of SL. Before giving details, we will outline the main idea behind the extension.
The AC decision procedure expects acyclicity, which prohibits formulae that are, e.g., of the form
(φ(x ) ∧φ ′ (y)) ∧ψ (x, y). Indeed, after replacing the inner-most conjunction by an equivalent rational
constraint, the formula turns into the conjunction Rφ∧φ ′ (x, y) ∧ Rψ (x, y), which is a conjunction of
the form R (x, y) ∧ S(x, y). In general, satisfiability of such conjunctions is not decidable, and theycannot be expressed as a single AFT since synchronisation of ϵ-moves on multiple tracks is notalways possible. However, our example conjunction does not compose two arbitrary AFTs. By its
construction, Rφ∧φ ′ (x, y) actually consists of two disjoint AFT parts. Each of the parts constrains
symbols read on one of the two tracks only and is completely oblivious of the other part. Due tothis, an AFT equivalent to Rφ∧φ ′ (x, y) ∧ Rψ (x, y) can be constructed (let us outline, without so far
going into details, that the construction would saturate ϵ-moves for each track of Rφ∧φ ′ separately).
Indeed, the original formula can also be rewritten as φ(x ) ∧ (φ(y) ∧ ψ (x, y)), which is AC and canbe solved by the algorithm of Section 5.
The idea of exploiting the independence of tracks within a transducer can be taken a step further.
The two independent parts do not have to be totally oblivious of each other, as in the case of Rφ∧φ ′above, but can communicate in a certain limited way. To define the allowed form of communicationand to make the independent communicating parts syntactically explicit within string formulae,
we will introduce the notion of synchronisation parameters of AFTs. We will then explain how
formulae built from constraints with synchronisation parameters can be transformed into a single
rational constraint with parameters by a simple adaptation of the AC algorithm, and how theparameters can be subsequently eliminated, leading to a single standard rational constraint.
Definition 6.1 (AFT with synchronisation parameters). An AFT with parameters s̄ = s 1 , . . . , sn isdefined as a standard AFT R = (V , Q, ∆, I, F ) with the difference that the initial and the final formula
can talk apart from states about so-called synchronisation parameters too. That is, I, F ⊆ FQ ∪{s̄ }where I is still positive on states and F is still negative on states, but the synchronisation parameters
can appear in I and F both positively as well as negatively. The synchronisation parameters put anadditional constraint on accepting runs. A run ρ = ρ 0 . . . ρm over a k-tuple of words w̄ is accepting
only if there is a truth assignment ν : {s̄} → B of parameters such that ν |= I and ν |= F . We thensay that w̄ is accepted with the parameter assignment ν .
String formulae can be built on top of AFTs with parameters in the same way as before. We write
φ[s̄](x̄ ) to denote a string formula that uses AFTs with synchronisation parameters from s̄ in its
rational constraints. Such a formula is interpreted over a union ι ∪ ν of an assignment ι : var(φ) →P (V ) ∗ from string variables to strings, as usual, and a parameter assignment ν : {s̄} → B. An atomic
15

constraint R[s̄](x̄ ) is satisfied by ι ∪ ν , written ι ∪ ν |= R[s̄](x̄ ), if R accepts (ι(x 1 ), . . . , ι(x |x̄ | )) withthe parameter assignment ν. Atomic string constraints without parameters are satisfied by ι ∪ ν iff
they are satisfied by ι. The satisfaction ι ∪ ν |= φ of a Boolean combination φ of atomic constraints
is then defined as usual.
Notice that within a non-trivial string formula, parameters may be shared among AFTs of several
rational constraints. They then not only synchronise initial and final configuration of a single
transducer run, but provide the aforementioned limited way of communication among AFTs of therational constraints within the formula.
Definition 6.2 (ACwith synchronisation parameters—ACsp). The definition of AC extends quite
straightforwardly to rational constraints with parameters. There is no other change in the definition
except for allowing rational constraints to use synchronisation parameters as defined above.
Notice that since we do not consider regular constraints with parameters, constraints withparameters in ACsp formulae are never negated.
The synchronisation parameters allow for an easier transformation of string formulae into AC.
For instance, consider a formula of the form φ(x, y) ∧ψ (x, y) where one of the conjuncts, say φ, canbe rewritten as φ 1 [s̄ 1 ](x ) ∧ φ 2 [s̄ 2 ](y). The whole formula can be written as φ 1 [s̄ 1 ](x ) ∧ (φ 2 [s̄ 2 ](y) ∧ψ (x, y)), which falls into ACsp. An example of such a formula φ(x, y), commonly found in thebenchmarks we experimented with as presented later on, is a formula saying that x ◦ y belongs
to a regular language, expressed by an AFA A. This can be easily expressed by a conjunction
R 1 [s̄](x ) ∧ R 2 [s̄](y) of two unary rational constraints with parameters. Intuitively, the AFTs R 1 andR 2 are two copies of A. R 1 nondeterministicaly chooses a configuration where the prefix of a runof A reading a word x ends, accepts, and remembers the accepting configuration in parametervalues (it will have a parameter per state). R 2 then reads the suffix of x, using the information
contained in parameter values to start from the configuration where R 1 ended. We explain thisconstruction in detail in Section 7.
An ACsp formula φ with parameters can be translated into a single, parameter-free, rational
constraint and then decided by an AFA language emptiness check described in Section 8. The
translation is done in two steps:(1) A generalised AC algorithm translates φ(x̄ ) to Rφ [s̄](x̄ ).
(2) Parameter elimination transforms Rφ [s̄](x̄ ) to a normal rational constraint Rφ′ (x̄ ).
Generalised AC algorithm. To enable eliminations of conjunctions and disjunctions from ACsp
formulae, just a small modification of the procedure from Section 5 is enough. The presenceof parameters in the initial and final formulae does not require any special treatment, except
that, unlike for states (which are implicitly renamed), it is important that sets of synchronisation
parameters stay the same even if they intersect, so that the synchronisation is preserved in the
resulting AFT. That is, for □ ∈ {∧, ∨}, Rφ [¯r ](x̄ ), and Rψ [s̄](ȳ), the constraint Rφ□ψ [t¯](z̄) is createdin the same way as described in Section 5, the parameters within the initial and the final formulaeof the input AFTs are passed to the AFA construction □ unchanged, and {t¯} = {¯r } ∪ {s̄}.
Lemma 6.3. Rφ [¯r ](x̄ ) □ Rψ [s̄](ȳ) is equivalent to Rφ□ψ [t¯](z̄).
Elimination of parameters. The previous steps transform the formula into a single rational constraint with synchronisation parameters. Within such a constraint, every parameter communicates
one bit of information between the initial and final configuration of a run. The bit can be encodedby an additional automata state passed from a configuration to a configuration via transitions
through the entire run, starting from an initial configuration where the parameter value is decidedin accordance with the initial formula, to the final configuration where it is checked against the final
16

formula. A technical complication, however, is that automata transitions are monotonic (positiveon states). Hence, they cannot prevent arbitrary states from appearing in target configurations
even though their presence is not enforced by the source configuration. For instance, startingfrom a single state q 1 and executing a transition ∆(q 1 ) = q 2 can yield a configuration q 2 ∧ q 3 . The
assignment of 0 to a parameter cannot therefore be passed through the run in the form of absenceof a single designated state as it can be overwritten anywhere during the run.
To circumvent the above, we use a so-called two rail encoding of parameter values: every parameters is encoded using a pair of value indicator states, the positive value indicator s + and the negativevalue indicator s − . Addition of unnecessary states into target configurations during a run then cannot
cause that a parameter silently changes its value. One of the indicators can still get unnecessarily set,but the other indicator will stay in the configuration too (states can be added into the configurations
reached, but cannot be removed). The parameter value thus becomes ambiguous—both s − and s + arepresent. The negative final formula can exclude all runs which arrive with ambiguous parameters
by enforcing that at least one of the indicators is false.
Formally, the parameter elimination replaces a constraint R (x̄ )[s̄] with R = (W ⟨|x̄ |⟩, Q, ∆, I , F )and |s̄ | = n by a parameter free constraint R ′ (x̄ ) with R ′ = (W ⟨|x̄ |⟩, Q ′, ∆ ′, I ′, F ′ ) where• Q ′ = Q ∪ {si+ , si− | 1 ≤ i ≤ n} (parameters are added to Q), and• ∆ ′ = ∆ ∪ {si+ 7→ si+ , si− 7→ si− | 1 ≤ i ≤ n} (once active value indicators stay active).
• I ′ = I + ∧ Choose where I + is a positive formula that arises from I by replacing every negative
occurrence of a parameter ¬s by a positive occurrence of its negative indicator s − , and theVpositive formula Choose = ni=1 si+ ∨ si− enforces that every parameter has a value.
• F ′ = F − ∧ Disambiguate where F − is a negative formula that arises from F by replacing every
positive occurence of a parameter s by a negative occurrence of its negative indicator ¬s − ,Vand the negative formula Disambiguate = ni=1 ¬si+ ∨ ¬si− enforces that indicators determine
parameter values unambiguously, i.e., at most one indicator per parameter is set.
Lemma 6.4. ∃s̄ : R (x̄ )[s̄] is equivalent to R ′ (x̄ ).
7

DECIDING STRAIGHT-LINE FORMULAE

Our algorithm solves string formulae using the DPLL(T) framework [Nieuwenhuis et al. 2004]6 ,where T is a sound and complete solver for AC and SL. Loosely speaking, DPLL(T) can be construed
as a collaboration between a DPLL-based SAT-solver and theory solvers, wherein the input formula
is viewed as a Boolean formula by the SAT solver, checked for satisfiability by the SAT-solver, and if
satisfiable, theory solvers are invoked to check if the Boolean assignment found by the SAT solver
can in fact be realised in the involved theories. The details of the DPLL(T) framework are not soimportant for our purpose. However, the crucial point is that all queries that a DPLL(T) solver asksa T-theory solver are conjunctions from the CNF of the input formula (or their parts), enabling us
to concentrate on solving SL conjunctions only.
Our decision procedure for SL conjunctions transforms the input SL conjunction into an equisatisfiable ACsp formula, which is then decided as discussed in Section 6. The rest of the section isthus devoted to a translation of a positive SL conjunction φ to an ACsp formula. The translationinternally combines rational constraints and equations into a more general kind of constraints inwhich rational relations are mixed with concatenations and synchronisation parameters.
Example 7.1. As a running example for the section, we use an SL conjunction that captures theessence of the vulnerability pattern from Example 1.1: A sanitizer is applied on an input string to
get rid of symbols c, replacing them by d, hoping that this will prevent a dangerous situation which
6 Also see [Kroening and Strichman 2008] for a gentle introduction to DPLL(T).

17arises when a symbol d apears in a string somewhere behind c. However, the dangerous situation
will not be completely avoided since it is forgotten that the sanitized string will be concatenatedwith another string that can still contain c.7
To formalize the example, assume a bit-vector encoding of an alphabet Σ which contains the
symbols c and d. Assume that each a ∈ Σ denotes the conjunction of (negated) bit variables encoding
it. As our running example, we will then consider the formula φ : y = R (x ) ∧ z = x ◦ y ∧ A (z). The
V
AFT R = (W ⟨2⟩, Q = {q}, ∆ = {q 7→ q ∧ ¬d1 ∧ (c1 → d2 ) ∧ a ∈Σ\{c} (a 1 ↔ a 2 ))}, I = q, F = true)is a sanitizer that produces y by replacing all occurrences of c in its input string x by d, and it also
makes sure that x does not include d. The AFA A = (V , Q ′ = {r 0 , r 1 , r 2 }, ∆ ′, I ′ = r 0 , F ′ = ¬r 0 ∧ ¬r 1 )where ∆ ′ (r 0 ) = (r 0 ∧¬c) ∨ (r 1 ∧c), ∆ ′ (r 1 ) = (r 1 ∧¬d) ∨ (r 2 ∧d), and ∆ ′ (r 2 ) = true is the specification.
It checks whether the opening symbol c can be later followed by the closing symbol d in the stringz. The formula is satisfiable.
□
Definition 7.2 (Mixed constraints). A mixed constraint is of the form x = R[s̄](y1 ◦ · · · ◦ yn ) where
R is a binary AFT, with a concatenation of variables as the right-hand side argument, and s̄ isa vector of synchronisation parameters. Such constraint has the expected meaning: it is satisfied
by the union ν ∪ ι of an assignment ι to string variables and an assignment ν to parameters iff(ι(x ), ι(y1 ) ◦ · · · ◦ ι(yn )) is accepted by R[s̄] with the parameter assignment ν .
All steps of our translation of the input SL formula φ to an ACsp formula preserve the SL fragment,
naturally generalised to mixed constraints as follows.
Definition 7.3 (Generalised straight-line conjunction). A conjunction of string constraints is definedV
to be generalised straight-line if it can be written as ψ ∧ m
i=1 x i = F i where ψ is a conjunction
over regular and negated regular constraints and each Fi is either of the form y1 ◦ · · · ◦ yn orR[s̄](y1 ◦ · · · ◦ yn ) such that it does not contain variables x i , . . . , xm .
For simplicity, we assume that φ has gone through two preprocessing steps. First, all negations
were eliminated by complementing regular constraints, resulting in a purely positive conjunction.
Second, all the—now only positive—regular constraints were replaced by equivalent rational constraints. Particularly, a regular constraint A(x ) is replaced by a rational constraint x ′ = R ′ (x )where x ′ is a fresh variable and R ′ is an AFT with Rel(R ′ ) = P (V ) ∗ × L(A). The AFT R ′ is createdfrom A by indexing all propositions in the transition relation by the index 2 of the second track.
It is not difficult to see that since x ′ is fresh, the replacement preserves SL, and also satisfiability,
since P (x ) ∧ ψ is equivalent to ∃x ′ : x ′ = R (x ) ∧ ψ for every ψ .
Example 7.4. In Example 7.1, the preprocessing replaces the conjunct A (z) by z ′ = S(z) where
S is the same as A, except occurrences of bit-vector variables in ∆ ′ are indexed by 2 since z will beread on its second track. We obtain φ 0′ : y = R (x ) ∧ z = x ◦ y ∧ z ′ = S(z) where z ′ is free.
□
Due to the preprocessing, we are starting with a formula φ 0′ in the form of an SL conjunction ofrational constraints and equations. The translation to ACsp will be carried out in the following
three steps, which will be detailed in the rest of the section:(1) Substitution transforms φ 0′ to a conjunction φ 1 of mixed constraints.
(2) Splitting transforms φ 1 to a conjunction φ 2 of rational constraints with parameters.
(3) Ordering transforms φ 2 to an AC conjunction φ 3 with parameters.
7 In reality, where one undesirably concatenates a string command(′ ... with some string ... ′ ); attack(); the situation is, ofcourse, more complex and sanitization is more sophisticated. However, having a real-life example, such as those used in our
experiments, as a running example would be too complex to understand.

18

Substitution. Equations in φ 0′ are combined with rational constraints into mixed constraints bya straightforward substitution. In one substitution step, a conjunction x = y1 ◦· · ·◦yn ∧ψ is replacedby ψ [y1 ◦ · · · ◦ yn /x] where all occurrences of x are replaced by y1 ◦ · · · ◦ yn . The substitution
preserves the generalised straight-line fragment.
Lemma 7.5. If x = y1 ◦ · · · ◦ yn ∧ ψ is SL, then ψ [y1 ◦ · · · ◦ yn /x] is equisatisfiable and SL.
The substitution steps are iterated eagerly in an arbitrary order until there are no equations.
Every substitution step obviously decreases the number of equations, so the iterative process
terminates after a finitely many steps with an equation-free SL conjunction of mixed constraints φ 1 .
Example 7.6. The substitution eliminates the equation z = x ◦ y in φ 0′ from Example 7.4, transforming it to φ 1 : y = R (x ) ∧ u = S(x ◦ y).
□
Splitting. We will now explain how synchronisation parameters are used to eliminate concatenation within mixed constraints. The operation of binary splitting applied to an SL conjunction of
mixed constraints, φ : x = R (y1 ◦ · · · ◦ ym ◦ z 1 ◦ · · · ◦ zn )[s̄] ∧ ψ , where R = (W ⟨2⟩, Q, ∆, I , F ) andQ = {q 1 , . . . , ql } splits the mixed constraint and substitutes x by a concatenation of fresh variables
x 1 ◦ x 2 in ψ . That is, it outputs the conjunction φ ′ : ζ ∧ ψ [x 1 ◦ x 2 /x] of mixed constraints, where
the rational constraint was split into the following conjunction ζ of two constraints:
ζ : x 1 = R 1 (y1 ◦ · · · ◦ ym )[s̄, t¯] ∧ x 2 = R 2 (z 1 ◦ · · · ◦ zn )[s̄, t¯]
The vector t¯ consists of l fresh parameters, x 1 and x 2 are fresh string variables, and each AFT withparameters Ri = (W ⟨2⟩, Q, ∆, Ii , Fi ), i ∈ {1, 2}, is derived from R by choosing initial/final formulae:
I 1 = I,

F1 =

l
^

qi → ti ,

I2 =

i=1

l
^

ti → qi ,F2 = F .

i=1

Intuitively, each run ρ of R is split into a run ρ 1 of R 1 , which corresponds to the first part of ρ inwhich y1 ◦ · · · ◦ ym is read along with a prefix x 1 of x, and a run ρ 2 of R 2 , which corresponds to thepart of ρ in which z 1 ◦ · · · ◦ zn is read along with the suffix x 2 of x. Using the new synchronisation
parameters t¯, the formulae F 1 and I 2 ensure that the run ρ 1 of R 1 must indeed start in the states inwhich the run ρ 2 of R 2 ended, that is, the original run ρ of R can be reconstructed by connecting
ρ 1 and ρ 2 . Every occurrence of x in ψ is replaced by the concatenation x 1 ◦ x 2 .
Lemma 7.7. In the above, φ is equivalent to ∃x 1x 2t¯ : φ ′.
The resulting formula φ ′ is hence equisatisfiable to the original φ. Moreover, φ ′ is still generalised
SL—the two new constraints defining x 1 and x 2 can be placed at the position of the original
constraint defining x that was split, and the substitution [x 1 ◦ x 2 /x] in the rest of the formula only
applies to the right-hand sides of constraints (since x can be defined only once).
Lemma 7.8. If φ is an SL conjunction of mixed constraints, then so is φ ′.
Moreover, by applying binary splitting steps eagerly in an arbitrary order on φ 1 , we are guaranteedthat all concatenations will be eliminated after a finite number of steps, thus arriving at the SL
conjunction of rational constraints with parameters φ 2 . The termination argument relies on thestraight-line restriction. Although it cannot be simply said that every step reduces the numberof concatenations because the substitution x 1 ◦ x 2 introduces new ones, the new concatenationsx 1 ◦ x 2 are introduced only into constraints defining variables that are higher in the straight-lineordering than x. It is therefore possible to define a well-founded (integer) measure on the formulaethat decreases with every application of the binary splitting steps.
19Lemma 7.9. All concatenations in the SL conjunction of mixed constraints φ 1 will be eliminatedafter a finite number of binary splitting steps.
We note that our implementation actually uses a slightly more efficient n-ary splitting instead ofthe described binary. It splits a mixed constraint in one step into the number of conjuncts equal
to the length of the concatenation in its right-hand side. We present the simpler binary variant,which eventually achieves the same effect.
Example 7.10. The formula from Example 7.6 would be transformed into φ 2 : y = R (x ) ∧ u 1 =V2(r i → s 0 )S1 [s̄](x ) ∧ S2 [s̄](y) where S1 , S2 are as S up to that S1 has the final formula I ′ ∧ i=0
V
2
and S2 has the final formula F ′ ∧ i=0(si → r i ). Notice that u 1 = S1 [s̄](x ) ∧ u 2 = S2 [s̄](y) still
enforce that x ◦ y has c eventually followed by d. The parameters remember where S1 ended its
run and force R 2 to continue from the same state.
□
Reordering modulo associativity. Substitution and splitting transform φ 0 to a straight-line conjunction φ 2 of rational constraints with parameters. Before delegating it to the ACsp formulae
solver, it must be reorganized modulo associativity to achieve a structure satisfying the definitionViof AC. One way of achieving this is to order the formula into a conjunction m
i=1 x i = R[s̄ ](yi )satisfying the condition in the definition of SL (the definition of SL only requires that the formulacan be assumed). An simple way is discussed in [Lin and Barceló 2016]. It consists of drawing thedependency graph of φ, a directed graph with the variables var(φ) as vertices which has an edge
x → y if and only if φ contains a conjunct x = R (y). Due to the straight-line restriction, the graphmust be acyclic. The ordering of variables can be then obtained as a topological sort of the graphs
vertices, which is computable in linear time (e.g. [Cormen et al. 2009], for instance by a depth-firstV
traversal). The final acyclic formula φ 3 then arises when letting m
i=1 associate from the right:
φ 3 : (x 1 = R 1 (y1 ) ∧ (x 2 = R 2 (y2 ) ∧ (. . . ∧ (xm−1 = Rm−1 (ym−1 ) ∧ xm = Rm (ym )) . . .))).
V
To see that φ 3 is indeed ACsp, observe that every conjunctive sub-formula is of the form ( i <k x i =Ri (yi )) ∧ x k = Rk (yk ) where x k is by the definition of SL not present in the left conjunct. The left
and right conjuncts can therefore share at most one variable, yk .
Theorem 7.11. The formula φ 3 obtained by substitution, splitting, and reordering from φ 0 is
equisatisfiable and acyclic.
Example 7.12. The ACsp formula φ 3 : y = R (x ) ∧ u 1 = S1 [s̄](x )) ∧ S2 [s̄](y) would be the final
result of the SL to ACsp translation. Let us use φ 3 to also briefly illustrate the decision procedure
for ACsp of Section 6. The first step is the transformation to a single rational constraint withparameters by induction over formula structure. This will produce R ′[s̄](x, y, z) with states andtransitions consisting of those in R, S1 with indexes of alphabet bits incremented by one (y, andz are now not the first and the second, but the second and the third track), and a copy S2′ of S2
with states replaced by their primed variant (so that they are disjoint from that of S1 ) and also
incremented indexes of alphabet bits. The initial and final configuration will be the conjunctions of
those of R, S1 and S2′ . The last step, eliminating of parameters, will lead to the addition of positive
and negative indicator states for parameters s̄ = s 1 , s 2 , s 3 with the universal self-loops and the
update of the initial and final formula as in Section 6. The rest is solved by the emptiness check
discussed in Section 8. Notice the small size of the resulting AFT. Compared to the original formulafrom Example 7.1, it contains only one additional copy of A (the S2′ ), the six additional parameter
indicator states with self-loops and the initial and final condition on the parameter indicators. □A note on the algorithm of [Lin and Barceló 2016]. We will now comment on the differences of
our algorithm for deciding SL from the earlier algorithm of [Lin and Barceló 2016]. It combines
reasoning on the level NFAs and nondeterministic transducers, utilising classical automata theoretic
20

techniques, with a technique for eliminating concatenation by enumerative automata splitting. It
first turns and SL formula into a pure AC formula and then uses the AC decision procedure.
An obvious advantage of our decision procedure described in Section 5 is the use of succinct
AFA. As opposed to the worst case exponentially larger NFA, it produces an AFA of a linear size
(unless the original formula contains negated regular constraints represented as general AFA. See
Section 5 for a detailed discussion). Let us also emphasize the advantages of our algorithm in thefirst phase, translation of SL to ACsp. Similarly as in the case of deciding AC, the main advantage
of our algorithm is that, while [Lin and Barceló 2016] only works with NFTs, we propose ways ofutilising the power of alternation and succinct transition encoding.
We will illustrate the difference on an example. The concatenation in the conjunction x =y ◦ z ∧ w = R (x ) would in [Lin and Barceló 2016] be done by enumerative splitting. It replaces theWconjunction by the disjunction q ∈Q w 1 = Rq (y) ∧ w 2 = q R (z). The Q in the disjunction is the setof states of the (nondeterministic) transducer R, Rq is the same as the NFT R up to that the final
state is q, and q R the same as R up to that the initial state is q. Intuitively, the run of R is explicitly
separated into the part in which y is read along the prefix w 1 of w, and the suffix in which z is red
along the suffix w 2 of w. The variable w would be replaced by w 1 ◦ w 2 in the rest of the formula.
The disjunction enumerates all admissible intermediate states q ∈ Q a run of R can cross, and foreach of them, it constructs two copies of R. This makes the cost of the transformation quadratic in
the number of states of the NFT R. A straightforward generalisation to our setting in which R is an
AFT is possible: The disjunction would have to list, instead of possible intermediate states q ∈ Q,
all possible intermediate configurations C ⊆ Q a run of the AFA R can cross, thus increasing thequadratic blow-up of the nondeterministic case to an exponential (due to the enumerative natureof splitting, the size is without any optimisation bounded by an exponential even from below).
Our splitting algorithm utilises succinctness of alternation to reduce the cost of enumerative
AFA splitting from exponential space (or quadratic in the case of NFAs) to linear. The smaller
size of the resulting representation is payed for by a more complex alternating structure of theresulting rational constraints. The worst case complexity of the satisfiability procedure thus remains
essentially the same. However, deferring most of the complexity to the last phase of the decision
procedure, AFA emptiness checking, allows to circumvent the potential blow-up by means ofmodern model checking algorithms and heuristics and achieve much better scalability in practice.
8

MODEL CHECKING FOR AFA LANGUAGE EMPTINESSIn order to check unsatisfiability of a string formula using our translation to AFTs, it is necessary toshow that the resulting AFT does not accept any word, i.e., that the recognised language is empty.
The constructed AFTs are succinct, but tend to be quite complex: a naïve algorithm that would
translate AFTs to NFAs using an explicit subset construction, followed by systematic state-space
exploration, is therefore unlikely to scale to realistic string problems. We discuss how the problemof AFT emptiness can instead be reduced (in linear time and space) to reachability in a Booleantransition system, in a way similar to [Cox and Leasure 2017; Gange et al. 2013; Wang et al. 2016].
Our translation is also inspired by the use of model checkers to determinise NFAs in [Tabakov andVardi 2005], by a translation to sequential circuits that corresponds to symbolic subset construction.
We use a similar implicit construction to map AFAs and AFTs to NFAs.
As an efficiency aspect of the construction for AFAs, we observe that it is enough to work withminimal sets of states, thanks to the monotonicity properties of AFAs (the fact that initial formulae
and transition formulae are positive in the state variables, and final formulae are negative). This
gives rise to three different versions: a direct translation that does not enforce minimality at all; anintensionally-minimal translation that only considers minimal sets by virtue of additional Boolean
21

constraints; and a deterministic translation that resolves nondeterminism through additional system
inputs, but does not ensure fully-minimal state sets.
8.1

Direct Translation to Transition Systems

To simplify the presentation of our translation to a Boolean transition system, we focus on thecase of AFAs A = (Vn , Q, ∆, I , F ) over a single track of bit-vectors of length n + 1. The translation
directly generalises to k-track AFTs, and to AFTs with epsilon characters, by simply choosing nsufficiently large to cover the bits of all tracks.
We adopt a standard Boolean transition system view on the execution of the AFA A (e.g., [Clarke
et al. 1999]). If A has m = |Q | automaton states, then A can be interpreted as a (symbolicallydi = (Bm , Init di , Trans di ). The transition system has state space Bm ,described) transition system T Ai.e., a system state is a bit-vector q̄ = ⟨q 0 , . . . , qm−1 ⟩ of length m identifying the active states in Q.
The initial states of the system are defined by Init di [q̄] = I , the same positive Boolean formula as in
A. The transition relation Transdi of the system is a Boolean formula over two copies q̄, q̄ ′ of thestate variables, encoding that for each active pre-state qi in q̄ the formula ∆(qi ) has to be satisfied
by the post-state q̄ ′. Input variables Vn = {x 0 , ..., x n } are existentially quantified in the transition
formula, expressing that all AFA transitions have to agree on the letter to be read:Transdi [q̄, q̄ ′] = ∃v 0 , . . . , vn :m−1^

qi → ∆(qi )[q̄/q̄ ′]

(1)

i=0
di can reach any state in the target
To examine emptiness of A, it has to be checked whether T A
diset Final [q̄] = F , i.e., in the set described by the negative final formula F of A. Since is well-known
that reachability in transition systems is a PSPACE-complete problem [Clarke et al. 1999], thisdirectly establishes that fragment AC is in PSPACE (Corollary 5.4).
di cannot reachLemma 8.1. The language L(A) recognised by the AFA A is empty if and only if T A
dia configuration in Final [q̄].

In practice, this means that emptiness of L(A) can be decided using a wide range of readily
available, highly optimised model checkers from the hardware verification field, utilising methods
such as k-induction [Sheeran et al. 2000], Craig interpolation [McMillan 2003], or IC3/PDR [Bradley
di in the AIGER format [Biere et al. 2017], and then2012]. In our implementation, we represent T A
apply nuXmv [Cavada et al. 2014] and ABC [Brayton and Mishchenko 2010].
di leaves room for optimisation, however, as it does not fully exploit the structure
The encoding T A
of AFAs and introduces more transitions than strictly necessary. In (1), we can observe that if
Transdi [q̄, q̄ ′] is satisfied for some q̄, q̄ ′, then it will also be satisfied for every post-state q̄ ′′ ⪰ q̄ ′,writing p̄ ⪯ q̄ for the point-wise order on bit-vectors p̄, q̄ ∈ Bm (i.e., p̄ ⪯ q̄ if pi implies qi for everyi ∈ {0, . . . , m − 1}). This is due to the positiveness (or monotonicity) of the transition formulae ∆(qi ).
Similarly, since the initial formula I of an AFA is positive, initially more states than necessary might
be activated. Because the final formula F is negative, and since redundant active states can only
impose additional restrictions on the possible runs of an AFA, such redundant states can never leadto more words being accepted.
di is well-structured [Finkel 1987],
More formally, we can observe that the transition system T A
mwhich means that the state space B can be equipped with a well-quasi-order ≤ such that wheneverTransdi [q̄, q̄ ′] and q̄ ≤ p̄, then there is some state p̄ ′ with q̄ ′ ≤ p̄ ′ and Transdi [p̄, p̄ ′]. In our case, ≤ isthe inverse point-wise order ⪰ on bit-vectors;8 intuitively, deactivating AFA states can only enable
more transitions. Since the set Final di [q̄] is upward-closed with respect to ≤ (downward-closed with
8 Since the state space Bm of T di is finite, the “well-” part is trivial.
A22respect to ⪯), the theory on well-structured transition systems tells us that it is enough to considertransitions to ≤-maximal states (or ⪯-minimal states) of the transition system when checking
di , the non-redundantreachability of Final di [q̄]. In forward-exploration of the reachable states of T A
states to be considered form an anti-chain. This can be exploited by defining tailor-made exploration
algorithms [Doyen and Raskin 2010; Kloos et al. 2013], or, as done in the next sections, by modifying
the transition system to only include non-redundant transitions.
8.2

Intensionally-Minimal Translation

di , by removing transitions to
We introduce several restricted versions of the transition system T A
minm
non-minimal states. The strongest transition system T A = (B , Init min , Transmin ) obtained in thisway can abstractly be defined as:

Init min [q̄] = Init di [q̄] ∧ ∀p̄ ≺ q̄. ¬Init di [p̄]Transmin [q̄, q̄ ′] = Transdi [q̄, q̄ ′] ∧ ∀p̄ ≺ q̄ ′ . ¬Transdi [q̄, p̄]

(2)
(3)

That means, Init min and Transmin are defined to only retain the ⪯-minimal states. Computing Init min
and Transmin corresponds to the logical problem of circumscription [McCarthy 1980], i.e., the computation of the set of minimal models of a formula. Circumscription is in general computationallyhard, and its precise complexity still open in many cases; in (2) and (3), note that eliminating theuniversal quantifiers (as well as the universal quantifiers introduced by negation of Transdi ) might
min does not directly appear useful as input
lead to an exponential increase in formula size, so that T A
to a model checker.
im = (Bm , Init im , Trans im ) by only minimising
We can derive a more practical, but weaker systemT A
post-states in Transim with respect to the same input letter Vn :Init im [q̄] = Init min [q̄]Transim [q̄, q̄ ′] = ∃ Vn . Trans[q̄, q̄ ′, Vn ] ∧ ∀p̄ ≺ q̄ ′ . ¬Trans[q̄, p̄, Vn ]withTrans[q̄, q̄ ′, Vn ] =m−1^

qi → ∆(qi )[q̄/q̄ ′]i=0

The formulae still contain universal quantifiers ∀p̄, but it turns out that the quantifiers can now
be eliminated with only polynomial effort, due to the fact that p̄ only occurs negatively in thescope of the quantifier. Indeed, whenever φ[q̄] is a formula that is positive in q̄, and φ[q̄] holds
for assignments q̄ 1 , q̄ 3 ∈ Bm with q̄ 1 ⪯ q̄ 3 , then φ[q̄] will also hold for any assignment q̄ 2 ∈ Bm
with q̄ 1 ⪯ q̄ 2 ⪯ q̄ 3 due to monotonicity. This implies that a satisfying assignment q̄ 1 ∈ Bm
is ⪯-minimal if no single bit in q̄ 1 can be switched from 1 to 0 without violating φ[q̄]. MoreV
formally, φ[q̄] ∧ ¬∃p̄ ≺ q̄. φ[p̄] is equivalent to φ[q̄] ∧ m−1
i=0 q i → ¬φ[q̄][q i /false], where wewrite φ[qi /false] for the result of substituting qi with false in φ.
The corresponding, purely existential representation of Init im and Transim is:
Init im [q̄] ≡ Init di [q̄] ∧m−1^

qi → ¬Init di [q̄][qi /false]

(4)

i=0
m−1


^
Transim [q̄, q̄ ′] ≡ ∃ Vn . Trans[q̄, q̄ ′, Vn ] ∧qi′ → ¬Trans[q̄, q̄ ′, Vn ][qi′ /false]

(5)

i=0

The representation is quadratic in size of the original formulae Init di , Transdi , but the formulae
can in practice be reduced drastically by sharing of common sub-formulae, since the m copies of
Init di [q̄][qi /false] and Trans[q̄, q̄ ′, Vn ][qi′ /false] tend to be almost identical.
23

Lemma 8.2. The following statements are equivalent:di can reach a configuration in Final di [q̄];(1) T Amin can reach a configuration in Final di [q̄];(2) T Aim can reach a configuration in Final di [q̄].
(3) T Aim encoding, we consider an AFA A that accepts the language
Example 8.3. To illustrate the T A{xwy | |xwy| = 2k, k ≥ 1, x ∈ {a, b}, y ∈ {c, d}} using the encoding of the alphabet Σ = {a, b, c, d }from Example 4.1. We let A = ({v 0 , v 1 }, {q 0 , q 1 , q 2 , q 3 , q 4 }, ∆, I, F ) where I = q 0 , F = ¬q 0 ∧¬q 1 ∧¬q 3(i.e., the accepting states are q 2 and q 4 ), and ∆ is defined as ∆(q 0 ) = ¬v 1 ∧ q 1 ∧ q 3 , ∆(q 1 ) = q 2 ,∆(q 2 ) = q 1 , ∆(q 3 ) = q 3 ∨ (v 1 ∧ q 4 ), and ∆(q 4 ) = false.
di = (B5 , Init di , Trans di ), defined by:
The direct transition system representation is T A

Init di [q̄] = q 0 ,(q 0 → ¬v 1 ∧ q ′ ∧ q 3′ ) ∧*. (q → q ′ ) ∧ 1
+/
1
2
.
//
Transdi [q̄, q̄ ′] = ∃v 0 , v 1 . .. (q 2 → q 1′ ) ∧.. (q → q ′ ∨ (v ∧ q ′ )) ∧ ///3
1
3
4, (q 4 → false)|{z}Trans[q̄, q̄ ′,Vn ]im can be derived from T di by conjoining the restrictions in
The intensionally-minimal translation T A
Aim′(4) and (5) (Trans [q̄, q̄ ] is shown in simplified form for sake of presentation):

Init im [q̄] = q 0 ∧ (q 0 → ¬false) ∧4^(qi → ¬q 0 ) ≡ q 0 ∧ ¬q 1 ∧ ¬q 2 ∧ ¬q 3 ∧ ¬q 4

i=1

Trans[q̄, q̄ ′, Vn ] ∧ ¬q 0′ ∧ (q 1′ → q 0 ∨ q 2 ) ∧ (q 2′ → q 1 ) ∧Trans [q̄, q̄ ] ≡ ∃v 0 , v 1 .
(q 3′ → q 0 ∨ (q 3 ∧ ¬(v 1 ∧ q 4′ ))) ∧ (q 4′ → q 3 ∧ ¬q 3′ )
im

!

′

□
8.3

Deterministic Translation

We introduce a further encoding of A as a transition system that is more compact than (4), (5), butdoes not always ensure fully-minimal state sets. The main idea of the encoding is that a conjunctive
transition formula ∆(q 1 ) = q 2 ∧ q 3 , assuming that q 2 , q 3 do not occur in any other transition
formula ∆(qi ), can be interpreted as a set of deterministic updates q 2′ = q 1 ; q 3′ = q 1 . For statevariables that occur in multiple transition formulae, the right-hand side of the update turns intoa disjunction. Disjunctions in transition formulae represent nondeterministic updates that canbe resolved using additional Boolean flags. The resulting transition system is deterministic, astransitions are uniquely determined by the pre-state and variables representing system inputs.
det = (Bm , Init det , Trans det ) using the AFA from ExExample 8.4. We illustrate the encoding T A
det
ample 8.3. While the initial states Init [q̄] coincide with Init im [q̄] in Example 8.3, the transition
relation Transdet [q̄, q̄ ′] now consists of two parts: a deterministic assignment of the post-state q̄ ′ interms of the pre-state q̄, together with an auxiliary variable h 3 that determines which branch of∆(q 3 ) is taken; and a conjunct that ensures that value of h 3 is consistent with the inputs Vn . The

24

resulting Transdet [q̄, q̄ ′] is (in this example) equivalent to Transim [q̄, q̄ ′]:Init det [q̄] = q 0 ∧ ¬q 1 ∧ ¬q 2 ∧ ¬q 3 ∧ ¬q 4
(q ′ ↔ false) ∧*. (q 0′ ↔ q ∨ q ) ∧+/(q 0 → ¬v 1 ) ∧
0
2
1
.
//
Transdet [q̄, q̄ ′] ≡ ∃h 3 . .. (q 2′ ↔ q 1 ) ∧∧ ∃v 0 , v 1 . *. (q 3 ∧ ¬h 3 → v 1 ) ∧ +//.. (q ′ ↔ q ∨ q ∧ h ) ∧ //0
3
3
, (q 4 → false)3′, (q 4 ↔ q 3 ∧ ¬h 3 )-□To define the encoding formally, we make the simplifying assumption that there is a uniqueinitial state q 0 , i.e., I = q 0 , and that all transition formulae ∆(qi ) are in negation normal form (i.e.,in particular state variables in ∆(qi ) do not occur underneath negation). Both assumption can be
det = (Bm , Init det , Trans det ) is:established by simple transformation of A. The transition system T A
Init det [q̄] = q 0 ∧

m−1
^

¬qi

i=1
 m−1
^

Transdet [q̄, q̄ ′] = ∃H . *
,


 m−1

^
qi′ ↔ NewState(qi ) ∧ ∃Vn .
qi → InputInv(∆(qi ), i) +
i=0
i=0
-

The transition relation Transdet consists of two main parts: the state updates, which assertthat every post-state variable qi′ is set to an update formula NewState(qi ); and an input invariant
asserting that the letters that are read are consistent with the transition taken. To determinise
disjunctions in transition formulae ∆(qi ), a set H of additional Boolean variables hl (uniquely
indexed by a position sequence l ∈ Z∗ ) is introduced, and existentially quantified in Transdet .
The update formulae NewState(qi ) are defined as a disjunction of assignments extracted fromthe transition formulae ∆(q j ),_NewState(qi ) ={φ | there is j ∈ {0, . . . , m − 1} such that ⟨qi , φ⟩ ∈ StateAsgn(∆(q j ), j, q j )}where each StateAsgn(∆(q j ), j, q j ) represents the set of asserted state variables qi in ∆(q j ), together
with guards φ for the case that qi occurs underneath disjunctions. The set is recursively defined(on formulae in NNF) as follows:
StateAsgn(φ 1 ∧ φ 2 , l, д) = StateAsgn(φ 1 , l, д) ∪ StateAsgn(φ 2 , l, д)StateAsgn(φ 1 ∨ φ 2 , l, д) = StateAsgn(φ 1 , l .1, д ∧ hl ) ∪ StateAsgn(φ 2 , l .2, д ∧ ¬hl )StateAsgn(qi , l, д) = {⟨qi , д⟩}StateAsgn(ϕ, l, д) = ∅(for any other ϕ) .

In particular, the case for disjunctions φ 1 ∨ φ 2 introduces a fresh variable hl ∈ H (indexed by
the position l of the disjunction) that controls which branch is taken. Input variables vi ∈ Vn are
ignored in the updates.
The input invariants InputInv(∆(qi ), i) are similarly defined recursively, and include the same
auxiliary variables hl ∈ H , but ensure input consistency:
InputInv(φ 1 ∧ φ 2 , l ) = InputInv(φ 1 , l ) ∧ InputInv(φ 2 , l ) InputInv(φ 1 ∨ φ 2 , l ) = hl → InputInv(φ 1 , l .1) ∧ ¬hl → InputInv(φ 2 , l .2)
InputInv(vi , l ) = vi , InputInv(¬vi , l ) = ¬vi , InputInv(qi , l ) = true, InputInv(ϕ, l ) = ϕ .
25

9IMPLEMENTATION AND EXPERIMENTS

We have implemented our method for deciding conjunctive AC and SL formulae as a solver called
Sloth (String LOgic THeory solver), extending the Princess SMT solver [Rümmer 2008]. The solver
Sloth can be obtained from https://github.com/uuverifiers/sloth/wiki. Hence, Princess provides us
with infrastructure such as an implementation of DPLL(T) or facilities for reading input formulaein the SMT-LIBv2 format [Barrett et al. 2010]. Like Princess, Sloth was implemented in Scala. We
present results from several settings of our tool featuring different optimizations.
Sloth-1 The basic version of Sloth, denoted as Sloth-1 below, uses the direct translation of the
AFA emptiness problem to checking reachability in transition systems described in Section 8.1.
Then, it employs the nuXmv model checker [Cavada et al. 2014] to solve the reachability problem
via the IC3 algorithm [Bradley 2012], based on property-directed state space approximation.
Further, we have implemented five optimizations/variants of the basic solver: four of them aredescribed below, the last one at the end of the section.
Sloth-2 Our first optimization, implemented in Sloth-2, is rather simple: We assume working
with strings over an alphabet Σ and look for equations of the form x = a 0 ◦ y1 ◦ a 1 . . . ◦ yn ◦ anwhere n ≥ 1, ∀0 ≤ i ≤ n : ai ∈ Σ∗ (i.e., ai are constant strings), and, for every 1 ≤ j ≤ n,
y j is a free string variable not used in any other constraint. The optimization replaces such
constraints by a regular constraint (a 0 ◦ Σ∗ ◦ a 1 . . . ◦ Σ∗ ◦ an )(x ). This step allows us to avoid
many split operations. The optimization is motivated by a frequent appearance of constraintsof the given kind in some of the considered benchmarks. As shown by our experimental results
below, the optimization yields very significant savings in practice, despite of its simplicity.
Sloth-3 Our second optimization, implemented in Sloth-3, replaces the use of nuXmv andIC3 in Sloth-2 by our own, rather simple model checker working directly on the generated
AFA. In particular, our model checker is used whenever no split operation is needed after the
preprocessing proposed in our first optimization. It works explicitly with sets of conjunctive state
formulae representing the configurations reached. The initial formula and transition formulae
are first converted to DNF using the Tseytin procedure. Then a SAT solver—in particular, sat4j[Berre and Parrain 2010]—is used to generate new reachable configurations and to check the
final condition. Our experimental results show that using this simple model checking approach
can win over the advanced IC3 algorithm on formulae without splitting.
Sloth-4 Our further optimization, Sloth-4, optimizes Sloth-3 by employing the intensionallyminimal successor computation of Section 8.2 within the IC3-based model checking of nuXmv.
Sloth-5 Finally, Sloth-5 modifies Sloth-4 by replacing the use of nuXmv with the property
directed reachability (i.e., IC3) implementation in the ABC tool [Brayton and Mishchenko 2010].
We present data on two benchmark groups (each consisting of two benchmark sets) that demonstrate two points. First, the main strength of our tool is shown on solving complex combinationsof transducer and concatenation constraints (generated from program code similar to that of
Example 1.1) that are beyond capabilities of any other solver. Second, we show that our tool iscompetitive also on simpler examples that can be handled by other tools (smaller constraints
with less intertwined and general combinations of rational and concatenation constraints). All thebenchmarks fall within the decidable straight-line fragment (possibly extended with the restricted
length constraints). All experiments were executed on a computer with Intel Xeon E5-2630v2 CPU@ 2.60 GHz and 32 GiB RAM.
Complex combinations of concatenation and rational constraints. The first set of our benchmarks
consisted of 10 formulae (5 sat and 5 unsat) derived manually from the PHP programs available
from the web page of the Stranger tool [Yu et al. 2010]. The property checked was absence26

of the vulnerability pattern .*<script.* in the output of the programs. The formulae contain
7–42 variables (average 21) and 7–38 atomic constraints (average 18). Apart from the Boolean
connectives ∧ and ∨, they use regular constraints, concatenation, the str.replaceall operation,and several special-purpose transducers encoding various PHP functions used in the programs(e.g., addslashes, trim, etc.).
Results of running the different verTable 1. PHP benchmarks from the web of Stranger.
sions of Sloth on the formulae are
Program #sat (sec) #unsat (sec) #mo #win +/shown in Table 1. Apart from the Sloth
Sloth-1
4 (178)
5 (6,989)
1
1/0
version used, the different columns
Sloth-2
4 (83)
5 (5,478)1
0/2
show numbers of solved sat/unsat for- Sloth-34 (72)
5 (3,673)
1
1/2
mulae (together with the time used), Sloth-44 (93)
4 (6,168)
20/0
numbers of out-of-memory runs (“mo”), Sloth-5
4 (324)4 (4,409)2
2/1
as well as numbers of sat/unsat instances for which the particular Sloth version provided the best result (“win +/-”). We can seethat Sloth was able to solve 9 out of the 10 formulae, and that each of its versions—apart from
Sloth-4—provided the best result in at least some case.
Our second benchmark consists of 8 challenging formulae taken from the paper [Kern 2014]providing an overview of XSS vulnerabilities in JavaScript programs (including the motivating
example from the introduction).
The formulae contain 9–12 variables (avTable 2. Benchmarks from [Kern 2014].
erage 9.75) and 9–13 atomic constraints
Solver#sat (sec) #unsat (sec) #win +/(average 10.5). Apart from conjunctions,
Sloth-1
4 (458)4 (583)
0/2
they use regular constraints, concatenaSloth-2
4 (483)4 (585)0/1
tion, str.replaceall, and again several
Sloth-3
4 (508)4 (907)
2/1
special-purpose transducers encoding variSloth-44 (445)4 (1,024)
1/0
ous JavaScript functions (e.g., htmlescape,Sloth-5
4 (568)4 (824)
1/0
escapeString, etc.). The results of our experiments are shown in Table 2. The meaning of the columns is the same as in Table 1 except that wedrop the out-of-memory column since Sloth could handle all the formulae—which we consider tobe an excellent result.
These results are the highlight of our experiments, taking into account that we are not aware of
any other tool capable of handling the logic fragment used in the formulae.9
A Comparison with other tools on simpler benchmarks. Our next benchmark consisted of 3,392
formulae provided to us by the authors of the Stranger tool. These formulae were derived by
Stranger from real web applications analyzed for security; to enable other tools to handle thebenchmarks, in the benchmarks the str.replaceall operation was approximated by str.replace.
Apart from the ∧ and ∨ connectives, the formulae use regular constraints, concatenation, and the
str.replace operation. They contain 1–211 string variables (on average 6.5) and 1–182 atomic
formulae (on average 5.8). Importantly, the use of concatenation is much less intertwined withstr.replace than it is with rational constraints in benchmarks from Tables 1 and 2 (only about
120 from the 3,392 examples contain str.replace). Results of experiments on this benchmark are
9 We tried to replace the special-purpose transducers by a sequence of str.replaceall operations in order to match thesyntactic fragment of the S3P solver [Trinh et al. 2016]. However, neither Sloth nor S3P could handle the modified formulae.
We have not experimented with other semi-decision procedures, such as those implemented within Stranger or SLOG
[Wang et al. 2016], since they are indeed a different kind of tool, and, moreover, often are not able to process input in the
SMT-LIBv2 format, which would complicate the experiments.

27

shown in Table 3. In the table, we compare the different versions of our Sloth, the S3P solver,
and the CVC4 string solver [Liang et al. 2014].10 The meaning of the columns is the same as in
the previous tables, except that we now specify both the number of time-outs (for a time-out of 5
minutes) and out-of-memory runs (“to/mo”).
From the results, we can see
Table 3. Benchmarks from Stranger with str.replace.
that CVC4 is winning, but (1) un- Solver#sat (sec) #unsat (sec) #to/mo #win +/like Sloth, it is a semi-decision
Sloth-1 1,200 (19,133) 2,079 (3,276)
105/8
30/43
procedure only, and (2) the for- Sloth-2 1,211 (13,120) 2,079 (3,338)
97/5
19/0
mulae of this benchmark are
Sloth-3 1,290 (6,619) 2,082 (1,012)
14/6
263/592
much simpler than in the previ- Sloth-4 1,288 (6,240) 2,082 (1,030)
17/5
230/327ous benchmarks (from the point
Sloth-5 1,291 (6,460)
2,082 (953)
14/5 768/1,120
of view of the operations used),
CVC4
1,297 (857)
2,082 (265)13/0–
and hence the power of Sloth
S3P
1,291 (171)2,078 (56)13/0–
cannot really manifest.
Despite that, our solver succeeds in almost the same number of examples as CVC4, and it isreasonably efficient. Moreover, a closer analysis of the results reveals that our solver won in 16
sat and 3 unsat instances. Compared with S3P, Sloth won in 22 sat and 4 unsat instances (plusS3P provided 8 unknown and 1 wrong answer and also crashed once). This shows that Sloth cancompete with semi-decision procedures at least in some cases even on a still quite simple fragmentof the logic it supports.
Our final set of benchmarks is
Table 4. Benchmarks from Stranger with str.replaceall.
obtained from the third one by fil- Program#sat (sec) #unsat (sec) #to/mo #win +/tering out the 120 examples con- Sloth-1 101 (1,404)
13 (18)6/0
9/1
taining str.replace and replac- Sloth-2 104 (1,178)
13 (18)3/0
8/5
ing the str.replace operations by
Sloth-3
103 (772)
13 (19)4/0
10/1
str.replaceall, which reflects the
Sloth-4
101 (316)
13 (23)
6/0
24/2
real semantics of the original pro- Sloth-5102 (520)
13 (20)5/0
52/4
grams. This makes the benchmarks
S3P
86 (11)
6 (26)
0/5–
more challenging, although they arestill simple compared to those of Tables 1 and 2. The results are shown in Table 4. The meaningof the columns is the same as in the previous tables. We compare the different versions of Slothagainst S3P only since CVC4 does not support str.replaceall. On the examples, S3P crashed
6 times and provided 6 times the unknown result and 13 times a wrong result. Overall, although
Sloth is still slower, it is more reliable than S3P (roughly 10 % of wrong and 10 % of inconclusive
results for S3P versus 0 % of wrong and 5 % of inconclusive results for Sloth).
As a final remark, we note that, apart from experimenting with the Sloth-1–5 versions, we also
tried a version obtained from Sloth-3 by replacing the intensionally minimal successor computationof Section 8.2 by the deterministic successor computation of Section 8.3. On the given benchmark,this version provided 3 times the best result. This underlines the fact that all of the described
optimizations can be useful in some cases.
10

CONCLUSIONS

We have presented the first practical algorithm for solving string constraints with concatenation,
general transduction, and regular constraints; the algorithm is at the same time a decision procedure
for the acyclic fragment AC of intersection of rational relations of [Barceló et al. 2013] and the
10 The S3P solver and CVC4 solvers are taken as two representatives of semi-decision procedures for the given fragmentwith input from SMT-LIBv2.

28

straight-line fragment SL of [Lin and Barceló 2016]. The algorithm uses novel ideas including
alternating finite automata as symbolic representations and the use of fast model checkers like IC3[Bradley 2012] for solving emptiness of alternating automata. In initial experiments, our solver
has shown to compare favourably with existing string solvers, both in terms of expressivenessand performance. More importantly, our solver can solve benchmarking examples that cannot be
handled by existing solvers.
There are several avenues planned for future work, including more general integration of length
constraints and support for practically relevant operations like splitting at delimiters and indexOf.
Extending our approach to incorporate a more general class of length constraints (e.g. Presburgerexpressible constraints) seems to be rather challenging since this possibly would require us toextend our notion of alternating finite automata with monotonic counters (see [Lin and Barceló
2016]), which (among others) introduces new problems on how to solve language emptiness.
ACKNOWLEDGMENTS
Holík and Janků were supported by the Czech Science Foundation (project 16-24707Y). Holík, Janků,and Vojnar were supported by the internal BUT grant agency (project FIT-S-17-4014) and the IT4IXS:
IT4Innovations Excellence in Science (project LQ1602). Lin was supported by European ResearchCouncil (ERC) under the European Union’s Horizon 2020 research and innovation programme(Grant Agreement no 759969). Rümmer was supported by the Swedish Research Council under
grant 2014-5484.
REFERENCES
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukás Holík, Ahmed Rezine, Philipp Rümmer, and Jari Stenman.
2014. String Constraints for Verification. In CAV. 150–166.
Davide Balzarotti, Marco Cova, Viktoria Felmetsger, Nenad Jovanovic, Engin Kirda, Christopher Kruegel, and Giovanni
Vigna. 2008. Saner: Composing Static and Dynamic Analysis to Validate Sanitization in Web Applications. In S&P.
387–401.
Pablo Barceló, Diego Figueira, and Leonid Libkin. 2013. Graph Logics with Rational Relations. Logical Methods in Computer
Science 9, 3 (2013). DOI:http://dx.doi.org/10.2168/LMCS-9(3:1)2013
Pablo Barceló, Leonid Libkin, A. W. Lin, and Peter T. Wood. 2012. Expressive Languages for Path Queries over GraphStructured Data. ACM Trans. Database Syst. 37, 4 (2012), 31.
Clark Barrett, Aaron Stump, and Cesare Tinelli. 2010. The SMT-LIB Standard: Version 2.0. In Proc. of SMT’10.
Clark W. Barrett, Cesare Tinelli, Morgan Deters, Tianyi Liang, Andrew Reynolds, and Nestan Tsiskaridze. 2016. Efficientsolving of string constraints for security analysis. In Proceedings of the Symposium and Bootcamp on the Science of Security,
Pittsburgh, PA, USA, April 19-21, 2016. 4–6. DOI:http://dx.doi.org/10.1145/2898375.2898393
Daniel Le Berre and Anne Parrain. 2010. The Sat4j library, release 2.2. JSAT 7, 2-3 (2010), 59–6. http://jsat.ewi.tudelft.nl/
content/volume7/JSAT7_4_LeBerre.pdf
Jean Berstel. 1979. Transductions and Context-Free Languages. Teubner-Verlag.
Armin Biere, Keijo Heljanko, and Siert Wieringa. 2017.
AIGER 1.9 and Beyond (Draft).
http://fmv.jku.at/hwmcc11/beyond1.pdf (cited in 2017). (2017).
Nikolaj Bjørner, Nikolai Tillmann, and Andrei Voronkov. 2009. Path feasibility analysis for string-manipulating programs.
In TACAS. 307–321.
Aaron R. Bradley. 2012. Understanding IC3. In Theory and Applications of Satisfiability Testing - SAT 2012 - 15th International
Conference, Trento, Italy, June 17-20, 2012. Proceedings. 1–14. DOI:http://dx.doi.org/10.1007/978-3-642-31612-8_1
Robert Brayton and Alan Mishchenko. 2010. ABC: An Academic Industrial-Strength Verification Tool. In Computer Aided
Verification: 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings, Tayssir Touili, Byron
Cook, and Paul Jackson (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 24–40. DOI:http://dx.doi.org/10.1007/
978-3-642-14295-6_5
Cristian Cadar, Vijay Ganesh, Peter M. Pawlowski, David L. Dill, and Dawson R. Engler. 2008. EXE: Automatically Generating
Inputs of Death. ACM Trans. Inf. Syst. Secur. 12, 2 (2008), 10:1–10:38. DOI:http://dx.doi.org/10.1145/1455518.1455522
Cristian Cadar, Patrice Godefroid, Sarfraz Khurshid, Corina S. Pasareanu, Koushik Sen, Nikolai Tillmann, and Willem
Visser. 2011. Symbolic execution for software testing in practice: preliminary assessment. In Proceedings of the 33rd

29

International Conference on Software Engineering, ICSE 2011, Waikiki, Honolulu , HI, USA, May 21-28, 2011. 1066–1071.
DOI:http://dx.doi.org/10.1145/1985793.1985995
Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover,
Marco Roveri, and Stefano Tonetta. 2014. The nuXmv Symbolic Model Checker. In CAV’14 (Lecture Notes in Computer
Science), Vol. 8559. Springer, 334–342.
Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. 1999. Model Checking. The MIT Press, Cambridge, Massachusetts.
Google co. 2015. Google Closure Library (referred in Nov 2015). https://developers.google.com/closure/library/. (2015).
Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. 2009. Introduction to Algorithms, Third Edition(3rd ed.). The MIT Press.
Arlen Cox and Jason Leasure. 2017. Model Checking Regular Language Constraints. CoRR abs/1708.09073 (2017).
arXiv:1708.09073 http://arxiv.org/abs/1708.09073
Loris D’Antoni, Zachary Kincaid, and Fang Wang. 2016. A Symbolic Decision Procedure for Symbolic Alternating Finite
Automata. CoRR abs/1610.01722 (2016). http://arxiv.org/abs/1610.01722
Loris D’Antoni and Margus Veanes. 2013. Static Analysis of String Encoders and Decoders. In VMCAI. 209–228.
Leonardo De Moura and Nikolaj Bjørner. 2011. Satisfiability modulo theories: introduction and applications. Commun.
ACM 54, 9 (2011), 69–77.
Volker Diekert. 2002. Makanin’s Algorithm. In Algebraic Combinatorics on Words, M. Lothaire (Ed.). Encyclopedia of
Mathematics and its Applications, Vol. 90. Cambridge University Press, Chapter 12, 387–442.
Laurent Doyen and Jean-François Raskin. 2010. Antichain Algorithms for Finite Automata. In TACAS’10 (Lecture Notes in
Computer Science), Vol. 6015. Springer, 2–22. DOI:http://dx.doi.org/10.1007/978-3-642-12002-2_2
Alain Finkel. 1987. A Generalization of the Procedure of Karp and Miller to Well Structured Transition Systems. In Automata,
Languages and Programming, 14th International Colloquium, ICALP87, Karlsruhe, Germany, July 13-17, 1987, Proceedings(Lecture Notes in Computer Science), Thomas Ottmann (Ed.), Vol. 267. Springer, 499–508. DOI:http://dx.doi.org/10.1007/
3-540-18088-5_43
Xiang Fu and Chung-Chih Li. 2010. Modeling Regular Replacement for String Constraint Solving. In NFM. 67–76.
Xiang Fu, Michael C. Powell, Michael Bantegui, and Chung-Chih Li. 2013. Simple linear string constraints. Formal Asp.
Comput. 25, 6 (2013), 847–891.
Vijay Ganesh, Mia Minnes, Armando Solar-Lezama, and Martin Rinard. 2013. Word equations with length constraints:
what’s decidable? In Hardware and Software: Verification and Testing. Springer, 209–226.
Graeme Gange, Jorge A. Navas, Peter J. Stuckey, Harald Søndergaard, and Peter Schachte. 2013. Unbounded Model-Checking
with Interpolation for Regular Language Constraints. In TACAS’2013 (Lecture Notes in Computer Science), Vol. 7795.
Springer, 277–291.
Seymour Ginsburg and Edwin H. Spanier. 1966. Semigroups, Presburger formulas, and languages. Pacific J. Math. 16, 2(1966), 285–296. http://projecteuclid.org/euclid.pjm/1102994974
Patrice Godefroid, Nils Klarlund, and Koushik Sen. 2005. DART: directed automated random testing. In Proceedings of the
ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation, Chicago, IL, USA, June 12-15, 2005.
213–223. DOI:http://dx.doi.org/10.1145/1065010.1065036
Claudio Gutiérrez. 1998. Solving Equations in Strings: On Makanin’s Algorithm. In LATIN. 358–373.
Mario Heiderich, Jörg Schwenk, Tilman Frosch, Jonas Magazinius, and Edward Z. Yang. 2013. mXSS attacks: attacking
well-secured web-applications by using innerHTML mutations. In CCS. 777–788.
Pieter Hooimeijer, Benjamin Livshits, David Molnar, Prateek Saxena, and Margus Veanes. 2011. Fast and Precise Sanitizer
Analysis with BEK. In USENIX Security Symposium. http://static.usenix.org/events/sec11/tech/full_papers/Hooimeijer.pdf
Pieter Hooimeijer and Westley Weimer. 2012. StrSolve: solving string constraints lazily. Autom. Softw. Eng. 19, 4 (2012),
531–559.
Artur Jez. 2016. Recompression: A Simple and Powerful Technique for Word Equations. J. ACM 63, 1 (2016), 4:1–4:51. DOI:
http://dx.doi.org/10.1145/2743014
Scott Kausler and Elena Sherman. 2014. Evaluation of String Constraint Solvers in the Context of Symbolic Execution. In
Proceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering (ASE ’14). ACM, New York,NY, USA, 259–270. DOI:http://dx.doi.org/10.1145/2642937.2643003
Christoph Kern. 2014. Securing the Tangled Web. Commun. ACM 57, 9 (Sept. 2014), 38–47.
Adam Kiezun and others. 2012. HAMPI: A solver for word equations over strings, regular expressions, and context-freegrammars. ACM Trans. Softw. Eng. Methodol. 21, 4 (2012), 25.
Nils Klarlund, Anders Møller, and Michael I. Schwartzbach. 2002. MONA Implementation Secrets. International Journal ofFoundations of Computer Science 13, 4 (2002), 571–586.
Johannes Kloos, Rupak Majumdar, Filip Niksic, and Ruzica Piskac. 2013. Incremental, Inductive Coverability. In CAV’13(Lecture Notes in Computer Science), Vol. 8044. Springer, 158–173.
Daniel Kroening and Ofer Strichman. 2008. Decision Procedures. Springer.

30

Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark Barrett, and Morgan Deters. 2014. A DPLL(T) Theory Solver for a
Theory of Strings and Regular Expressions. In CAV. 646–662.
Tianyi Liang, Andrew Reynolds, Nestan Tsiskaridze, Cesare Tinelli, Clark Barrett, and Morgan Deters. 2016. An efficient
SMT solver for string constraints. Formal Methods in System Design 48, 3 (2016), 206–234. DOI:http://dx.doi.org/10.1007/
s10703-016-0247-6
Tianyi Liang, Nestan Tsiskaridze, Andrew Reynolds, Cesare Tinelli, and Clark Barrett. 2015. A Decision Procedure for Regular
Membership and Length Constraints over Unbounded Strings. In Frontiers of Combining Systems - 10th International
Symposium, FroCoS 2015, Wroclaw, Poland, September 21-24, 2015. Proceedings. 135–150. DOI:http://dx.doi.org/10.1007/
978-3-319-24246-0_9
Anthony Widjaja Lin and Pablo Barceló. 2016. String solving with word equations and transducers: towards a logic for
analysing mutation XSS. In POPL. 123–136. DOI:http://dx.doi.org/10.1145/2837614.2837641
Blake Loring, Duncan Mitchell, and Johannes Kinder. 2017. ExpoSE: Practical Symbolic Execution of Standalone JavaScript.
In SPIN.
Gennady S Makanin. 1977. The problem of solvability of equations in a free semigroup. Sbornik: Mathematics 32, 2 (1977),
129–198.
John McCarthy. 1980. Circumscription - A Form of Non-Monotonic Reasoning. Artif. Intell. 13, 1-2 (1980), 27–39. DOI:
http://dx.doi.org/10.1016/0004-3702(80)90011-9
Kenneth L. McMillan. 2003. Interpolation and SAT-Based Model Checking. In Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings. 1–13. DOI:http://dx.doi.org/10.1007/
978-3-540-45069-6_1
Christophe Morvan. 2000. On Rational Graphs. In FoSSaCS. 252–266.
Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli. 2004. Abstract DPLL and Abstract DPLL Modulo Theories. In
LPAR’04 (LNCS), Vol. 3452. Springer, 36–50.
OWASP. 2013. https://www.owasp.org/images/f/f8/OWASP_Top_10_-_2013.pdf. (2013).
Wojciech Plandowski. 2004. Satisfiability of word equations with constants is in PSPACE. J. ACM 51, 3 (2004), 483–496.
Wojciech Plandowski. 2006. An efficient algorithm for solving word equations. In STOC. 467–476.
Gideon Redelinghuys, Willem Visser, and Jaco Geldenhuys. 2012. Symbolic execution of programs with strings. In SAICSIT.
139–148.
Philipp Rümmer. 2008. A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic. In Proceedings,
15th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LNCS), Vol. 5330. Springer,
274–289.
Jacques Sakarovitch. 2009. Elements of automata theory. Cambridge University Press.
Prateek Saxena, Devdatta Akhawe, Steve Hanna, Feng Mao, Stephen McCamant, and Dawn Song. 2010. A Symbolic
Execution Framework for JavaScript. In S&P. 513–528.
Koushik Sen, Swaroop Kalasapur, Tasneem G. Brutch, and Simon Gibbs. 2013. Jalangi: a selective record-replay and dynamic
analysis framework for JavaScript. In Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT
Symposium on the Foundations of Software Engineering, ESEC/FSE’13, Saint Petersburg, Russian Federation, August 18-26,
2013. 488–498. DOI:http://dx.doi.org/10.1145/2491411.2491447
Mary Sheeran, Satnam Singh, and Gunnar Stålmarck. 2000. Checking Safety Properties Using Induction and a SAT-Solver.
In FMCAD (LNCS), Vol. 1954. Springer, 108–125.
Deian Tabakov and Moshe Y. Vardi. 2005. Experimental Evaluation of Classical Automata Constructions. In Logic for
Programming, Artificial Intelligence, and Reasoning, 12th International Conference, LPAR 2005, Montego Bay, Jamaica,
December 2-6, 2005, Proceedings (Lecture Notes in Computer Science), Geoff Sutcliffe and Andrei Voronkov (Eds.), Vol. 3835.
Springer, 396–411. DOI:http://dx.doi.org/10.1007/11591191_28
Minh-Thai Trinh, Duc-Hiep Chu, and Joxan Jaffar. 2014. S3: A Symbolic String Solver for Vulnerability Detection in Web
Applications. In CCS. 1232–1243.
Minh-Thai Trinh, Duc-Hiep Chu, and Joxan Jaffar. 2016. Progressive Reasoning over Recursively-Defined Strings. In
Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings,
Part I. 218–240. DOI:http://dx.doi.org/10.1007/978-3-319-41528-4_12
Moshe Y. Vardi. 1995. An Automata-Theoretic Approach to Linear Temporal Logic. In Logics for Concurrency - Structure
versus Automata (8th Banff Higher Order Workshop, August 27 - September 3, 1995, Proceedings). 238–266. DOI:http://dx.doi.org/10.1007/3-540-60915-6_6
Margus Veanes, Pieter Hooimeijer, Benjamin Livshits, David Molnar, and Nikolaj Bjørner. 2012. Symbolic finite statetransducers: algorithms and applications. In POPL. 137–150.
Hung-En Wang, Tzung-Lin Tsai, Chun-Han Lin, Fang Yu, and Jie-Hong R. Jiang. 2016. String Analysis via Automata
Manipulation with Logic Circuit Representation. In Computer Aided Verification - 28th International Conference, CAV
2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I (Lecture Notes in Computer Science), Vol. 9779. Springer,31241–260. DOI:http://dx.doi.org/10.1007/978-3-319-41528-4
Gary Wassermann, Dachuan Yu, Ajay Chander, Dinakar Dhurjati, Hiroshi Inamura, and Zhendong Su. 2008. Dynamic test
input generation for web applications. In ISSTA. 249–260.
Joel Weinberger, Prateek Saxena, Devdatta Akhawe, Matthew Finifter, Eui Chul Richard Shin, and Dawn Song. 2011. A
Systematic Analysis of XSS Sanitization in Web Application Frameworks. In ESORICS. 150–171.
Fang Yu, Muath Alkhalaf, and Tevfik Bultan. 2010. Stranger: An Automata-Based String Analysis Tool for PHP. In TACAS.
154–157. Benchmark can be found at http://www.cs.ucsb.edu/~vlab/stranger/.
Fang Yu, Muath Alkhalaf, Tevfik Bultan, and Oscar H. Ibarra. 2014. Automata-based symbolic string analysis for vulnerability
detection. Formal Methods in System Design 44, 1 (2014), 44–70.
Fang Yu, Tevfik Bultan, and Oscar H. Ibarra. 2009. Symbolic String Verification: Combining String Analysis and Size Analysis.
In TACAS. 322–336.
Fang Yu, Tevfik Bultan, and Oscar H. Ibarra. 2011. Relational String Verification Using Multi-Track Automata. Int. J. Found.
Comput. Sci. 22, 8 (2011), 1909–1924.
Yunhui Zheng, Xiangyu Zhang, and Vijay Ganesh. 2013. Z3-str: a Z3-based string solver for web application analysis. In
ESEC/SIGSOFT FSE. 114–124.

Appendix
A

PROOF OF LEMMA 7.9
Proof. Given an SL conjunction of mixed constraints written in the wayn^iφ:x i = Ri [s̄ i ](y1i ◦ · · · ◦ ym)ii=1

which satisfies the condition in the definition of SL, we define its weight as the sum of weights of
its variablesX
W (φ) =W (x )x ∈var(φ )where the weight of a variable x i , 1 ≤ i ≤ n, is defined as
W (x i ) = (mi − 1) +

mi
X
j=1

W (y ij ),and the weight of a variable x ∈ var(φ) \ {x 1 , . . . , x n } as W (x ) = 0. That is, the weight of x i isderived from its defining constraint as the sum of the weights of the concatenated variables andthe number of concatenation operators used.
Let the binary splitting step replace x i = R (y1 ◦ · · · ◦ ym ◦ z 1 ◦ · · · ◦ zl )[s̄ i ] in φ by x 1′ =R 1 (y1 ◦ · · · ◦ ym )[s̄ i , t¯] ∧ x 2′ = R 2 (z 1 ◦ · · · ◦ zl )[s̄ i , t¯], while replacing every other occurrence ofx i by x 1′ ◦ x 2′ , producing the formula φ ′. Let us analyse how the splitting influenced the weights.
First, observe that the weights of variables x k for k < i and of the undefined variables outside{x 1 , . . . , x n } do not change since they do not depend on x i , by the definition of SL. Hence, theweights of all variables y1 , . . . , ym and z 1 , . . . , zl that define W (x i ) do not change. Since x i is invar(φ ′ ) replaced by x 1′ and x 2′ , the weight W (x i ) of x i from the sum defining W (φ) is in the sum
defining W (φ) ′ replaced by W (x 1′ ) + W (x 2′ ). Observe that due to the −1 factor in the definition ofa weight of a variable, the second number is smaller by one:W (x i ) = (m + l − 1) +

m
X
j=1

W (y j ) +lX

W (z j ) >

j=1
m
l

 

X
X
> (m − 1) +W (y j ) + (l − 1) +W (z j ) = W (x 1′ ) + W (x 2′ )
j=1

j=1

32

In the defining constraints of variables x k , k > i, x i is replaced by x 1′ ◦ x 2′ ; hence, in the sum
defining W (x k ), W (x i ) is replaced by W (x 1′ ) + W (x 2′ ) + 1 (where the +1 is for the one occurrenceof concatenation) which is, by the previous analysis, equal to W (x i ). The weights of variables x k ,k > i, in φ ′ are therefore the same as in φ. Since weights of all variables in var(φ) are the same forboth formulae, the only difference between the formulae weights is that between W (x i ) in φ andW (x 1′ ) + W (x 2′ ) in φ ′. It must therefore hold that W (φ) > W (φ ′ ).
Additionally, observe that W (φ) can obviously never be smaller than 0 since W (x ) ≥ 0 for everyx ∈ var(φ). This can be shown by an easy induction on n. That concludes the proof.
□33