CertiStr: A Certified String Solver
Shuanglong Kan

Anthony W. Lin

Department of Computer Science
Technische Universität Kaiserslautern
Kaiserslautern, Germany
shuanglong@cs.uni-kl.de

Department of Computer Science
Technische Universität Kaiserslautern & MPI-SWS
Kaiserslautern, Germany
lin@cs.uni-kl.de

Philipp Rümmer

Micha Schrader

Department of Information Technology
Uppsala University
Uppsala, Sweden
philipp.ruemmer@it.uu.se

Department of Computer Science
Technische Universität Kaiserslautern
Kaiserslautern, Germany
schrader@rhrk.uni-kl.de

Abstract
Theories over strings are among the most heavily researched
logical theories in the SMT community in the past decade,owing to the error-prone nature of string manipulations,which often leads to security vulnerabilities (e.g. cross-site
scripting and code injection). The majority of the existing
decision procedures and solvers for these theories are themselves intricate; they are complicated algorithmically, andalso have to deal with a very rich vocabulary of operations.
This has led to a plethora of bugs in implementation, whichhave for instance been discovered through fuzzing.
In this paper, we present CertiStr, a certified implementation of a string constraint solver for the theory of strings withconcatenation and regular constraints. CertiStr aims to solve
string constraints using a forward-propagation algorithm
based on symbolic representations of regular constraints as
symbolic automata, which returns three results: sat, unsat,
and unknown, and is guaranteed to terminate for the string
constraints whose concatenation dependencies are acyclic.
The implementation has been developed and proven correct
in Isabelle/HOL, through which an effective solver in OCaml
was generated. We demonstrate the effectiveness and efficiency of CertiStr against the standard Kaluza benchmark,in which 80.4% tests are in the string constraint fragment ofCertiStr. Of these 80.4% tests, CertiStr can solve 83.5% (i.e.
CertiStr returns sat or unsat) within 60s.
CCS Concepts: • Theory of computation → Automatedreasoning; Formal languages and automata theory.

Permission to make digital or hard copies of part or all of this work forpersonal 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 the full citation on the first page. Copyrights for thirdparty components of this work must be honored. For all other uses, contact
the owner/author(s).
CPP ’22, January 17–18, 2022, Philadelphia, PA, USA© 2022 Copyright held by the owner/author(s).
ACM ISBN 978-1-4503-9182-5/22/01.
https://doi.org/10.1145/3497775.3503691

Keywords: string theory, Isabelle, symbolic automata, SMT
solvers
ACM Reference Format:
Shuanglong Kan, Anthony W. Lin, Philipp Rümmer, and Micha
Schrader. 2022. CertiStr: A Certified String Solver. In Proceedingsof the 11th ACM SIGPLAN International Conference on Certified
Programs and Proofs (CPP ’22), January 17–18, 2022, Philadelphia,
PA, USA. ACM, New York, NY, USA, 15 pages. https://doi.org/10.
1145/3497775.3503691

1

Introduction

Strings are among the most fundamental and commonlyused data types in virtually all modern programming languages, especially with the rapidly growing popularity of dynamic languages, including JavaScript and Python. Programs
written in such languages often implement security-criticalinfrastructure, for instance web applications, and they tend
to process data and code in string representation by applying built-in string-manipulating functions; for instance, tosplit, concatenate, encode/decode, match, or replace parts ofa string. Functions of this kind are complex to reason about
and can easily lead to programming mistakes. In some cases,
such mistakes can have serious consequences, e.g., in thecase of web applications, cross-site scripting (XSS) attacks
can be used by a malicious user to attack both the web serveror the browsers of other users.
One promising research direction, which has been intensively pursued in the SMT community in the past ten years,
is the development of SMT solvers for theories of strings(dubbed string solvers) including Kaluza [35], CVC4 [28],Z3 [17], Z3-str3 [4], Z3-Trau [9], S3P [39], OSTRICH [13],SLOTH [22], and Norn [1], to name only a few. Such solvers
are highly optimized and find application, among others,
in bounded model checkers and symbolic execution tools[14, 34], but also in tools tailored to verification of the security properties [3].
It has long been observed that constraint solvers are extremely complicated procedures, and that implementations

CPP ’22, January 17–18, 2022, Philadelphia, PA, USA

Shuanglong Kan, Anthony W. Lin, Philipp Rümmer, and Micha Schraderare prone to bugs. Defects that affect soundness or completeness are routinely found even in well-maintained state-ofthe-art tools, both in real-world applications and throughtechniques like fuzzing [6, 8, 31]. String solvers are particularly troublesome in this context, since, unlike other SMT
theories, the theory of strings requires a multitude of operations including concatenation, regular constraints, string
replacement, length constraints, and many others. This inherent intricacy is also reflected in the recently developed SMTLIB standard for strings (http://smtlib.cs.uiowa.edu/theoriesUnicodeStrings.shtml). Many of the string solvers that arosein the past decade relied on inevitably intricate decision procedures, which resulted in subtle bugs in implementations
themselves even among the mainstream string solvers (e.g.
see [8, 31]). This implies the unfortunate fact that one cannot
blindly trust the answer provided by string solvers.

Non-deterministic Finite Automata (NFA) by allowing transition labels to be a set of characters in the (potentially infinite)alphabet, represented by an element of a boolean algebra(e.g. the interval algebra or the BDD algebra), instead of asingle character. s-NFAs are especially crucial for an efficient
implementation of automata-based string solving algorithms
and many string processing algorithms [1, 13, 16, 24, 41],for which reason our certified implementation of an s-NFA
library is of independent interests.
Last but not least, we have automatically generated a verified implementation CertiStr in Isabelle/HOL, which wehave extensively evaluated against the standard string solving benchmark from Kaluza [35] with around 38000 string
constraints. For the first time, we demonstrate that the simple forward-propagation algorithm in fact performs surprisingly well even compared to other highly optimized solvers(which are not verified implementations). In particular, weshow that the majority of these constraints (83.5%) are solved
by CertiStr; for the rest, the tool either returns unknown, or
times out. Moreover, CertiStr terminates within 60 seconds
on 98% of the constraints, witnessing its efficiency.
To summarize, our contributions are:Contributions. In this paper, we present CertiStr, thefirst certified implementation of a string solver for the standard theory of strings with concatenation and regular constraints (a.k.a. word equations with regular constraints [18,20, 23, 30]). CertiStr aims to solve string constraints by meansof the so-called forward-propagation algorithm, which relies on a simple idea of propagating regular constraints
in a forward direction in order to derive contradiction, or
prove the absence thereof (see Section 2 for an example).
Similar ideas are already present in abstract interpretationof string-manipulating programs (e.g. see [32, 42, 43]), but
not yet at the level of string solvers, i.e., which operate on
string constraints. We have proven in Isabelle/HOL [33]some crucial properties of the forward-propagation algorithm and more specifically with respect to our implementation CertiStr: (i) [TERMINATION]: the algorithm terminates
on string constraints without cyclic concatenation dependencies, (ii) [SOUNDNESS]: CertiStr is sound for unsatisfiable results (if forward-propagation detects inconsistencies
in a constraint, then the constraint is indeed unsatisfiable),and (iii) [COMPLETENESS]: CertiStr is complete for constraints satisfying the tree property (i.e., in which on theright-hand side of each equation every variable appears at
most once). Here completeness amounts to the fact that, if
forward-propagation does not detect inconsistencies for aconstraint satisfying the tree property, then the constraint is
indeed satisfiable. For the constraints that do not satisfy thetree property and CertiStr cannot decide them as unsatisfiable,
CertiStr returns unknown.
In order to facilitate the propagation of regular constraints,
we also implement a certified library for Symbolic Nondeterministic Finite Automata (s-NFA), which contains various automata operations, such as the concatenation andproduct of two s-NFAs, the language emptiness checking fors-NFAs, among others. s-NFAs — as introduced by Veanes etal. [41] (see [16] for more details) — are different from classic• we developed in Isabelle/HOL the tool CertiStr, thefirst certified implementation of a string solver.
• we implemented the first certified symbolic automata
library, which is crucial for an efficient implementationof many string processing applications [16].
• CertiStr was evaluated over Kaluza benchmark [35],with around 38000 tests. In this benchmark, 83.5% of
the tests can be solved with the results sat or unsat.
Moreover, the solver terminates within 60 seconds on
98% of the tests, witnessing the surprising competitiveness of the simple forward-propagation algorithm
against more complicated algorithms.

2

Motivating Example

We start by illustrating the decision procedure implemented
by CertiStr. CertiStr uses the so-called forward-propagation
algorithm for solving satisfiability of string theory with concatenation and regular membership constraints. To illustrate
the algorithm, consider the formula:domain ∈ /[a-zA-Z.]+/(1)∧ dir, file ∈ /[a-zA-Z0-9.]+/(2)∧

path = dir + "/" + file(3)∧

url = "http://" + domain + "/" + path

(4)

[∧

url ∈ /.*<script>.*/](5)

The formula contains string variables (domain, dir, etc.),
and uses both regular membership constraints and word
equations with concatenation to model the construction of a
URL from individual components. Regular expressions are
written using the standard PCRE syntax (https://perldoc.perl.

CertiStr: A Certified String Solver

CPP ’22, January 17–18, 2022, Philadelphia, PA, USA

org/perlre). Each equation should be read as an assignmentof the right-hand side term to the left-hand side variable,
and is processed in this direction. We initially ignore theconstraint (5).
The forward-propagation algorithm propagates regularmembership constraints and derives new constraints for thevariable on the left-hand side of equations. In this example, the algorithm starts with equation (3) and propagatesconstraint (2), resulting in the new constraint
path ∈ /[a-zA-Z0-9.]+\/[a-zA-Z0-9.]+/(6)

We can propagate this new constraint further, using equation (4) and together with constraint (1), deriving:url ∈ /http:\/\/[a-zA-Z.]+\/[a-zA-Z0-9.]+\/[a-zA-Z0-9.]+/(7)

At this point, no more propagations are possible. Note thatforward-propagation will terminate, in general, wheneverno cyclic dependencies exist between the equations, whichis the fragment of formulas we consider.
Still ignoring (5), we can observe that forward-propagation
has not discovered any inconsistent constraints. In order
to conclude the satisfiability of the formula from this, weneed a meta-result about forward-propagation: we showthat forward propagation is complete for acyclic formulasin which each variable occurs at most once on the righthand side of equations. Since this criterion holds for theformula (1) ∧ · · · ∧ (4), we have indeed proven that it issatisfiable.
Consider now also (5), modelling a simple form of injection attack. We can observe that this additional constraint isinconsistent with the derived constraint (7), since the intersection of the asserted regular languages is empty. Forwardpropagation detects this conflict as soon as (7) has been computed: each time a new membership constraint is derived,
the algorithm will check the consistency with constraints already assumed. Since we also show that forward-propagation
is sound w.r.t. inconsistency, the detection of a conflict immediately implies that the formula (1) ∧ · · · ∧ (5) is unsatisfiable.
In summary, the forward-propagation is defined using two
main inference steps: the post-image computation for word
equations, and a consistency check for regular constraints.
Although the example uses regular expressions, both operations can be defined more easily through a translation tofinite-state automata. To obtain a verified string solver, theimplementation of both operations has to be shown correct,
and in addition meta-results need to be derived about thesoundness and completeness of the overall algorithm.
We can also observe that classical finite-state automata,over concrete alphabets, are cumbersome even for toy examples; regular expressions often talk about character ranges
that would require a large number of individual transitions.
In practice, string constraints are usually formulated over the

Unicode alphabet with currently 3×216 characters, which necessitates symbolic character representation. In our verified
implementation, we therefore use a simple form of symbolic
automata [15] in which transitions are labelled with character intervals.

3

String Constraint Fragment

In this section, we present the string constraint fragmentthat CertiStr supports and its semantics of satisfiability.
Let Σ be an alphabet and Σ∗ denote the set of words over Σ.
Let w 1 , w 2 ∈ Σ∗ be two words, w 1w 2 denotes the concatenation of the two words, i.e., w 2 is appended to the end of w 1 toget a new string. We consider the following string constraint
language over Σ:c ::= x ∈ A | x = x 1 + x 2 | c 1 ∧ c 2 ,where x denotes a variable ranging over Σ∗ and A denotes an
NFA representing a regular language over Σ. The language
accepted by A is denoted by L(A). The semantics of aconstraint c is defined in an obvious way by interpreting x ∈A as a membership of x in the language L(A), x = x 1 + x 2
as a string equation, and c 1 ∧ c 2 as a conjunction of c 1 andc 2 . More precisely, given a function µ mapping each variablein the constraint c to a string in Σ∗ , we say that µ satisfies
c if: (i) µ (x ) ∈ L(A) for each constraint x ∈ A in c, and(ii) µ (x ) = µ (x 1 )µ (x 2 ) for each constraint x = x 1 + x 2 . The
constraint c is satisfiable if one such solution µ for c exists.
Our string constraint language is as general as word equations with regular constraints [18, 20, 23, 30], which forms
the basis of the recently published Unicode string constraint
language in SMT-LIB 2.6, and already makes up the bulk of
existing string constraint benchmarks. Notice that our restriction to string equation of the form x = x 1 +x 2 is not a real
restriction since general string constraints can be obtained bymeans of desugaring. For instance, the concatenation of morethan two variables, like x = x 1 + x 2 + x 3 can be desugared as
two concatenation constraints: (1) x ′ = x 1 + x 2 ; x = x ′ + x3.
Moreover, a subset of string constraints with length functions(called monadic length) can also be translated into this fragment with regular constraints. For instance, |x | ≤ 6, where|x | denotes the length of the word of x, can be translated toa regular membership constraint as x ∈ A, where A is an
NFA that accepts any word whose length is at most 6. Recent experimental evidence shows that a substantial portionof length constraints that appear in practice are essentiallymonadic [21]. There are also some string constraints using
disjunction (∨). For instance, c 1 ∨ c 2 , where c 1 and c 2 are
string constraints in our fragment. This also can be solved
with CertiStr by first solving c 1 and c 2 separately, and thenchecking whether one of them is satisfiable.
Figure 1 shows the framework of CertiStr. The input of
the solver is an SMT file with string constraints. The tool
has two parts: (1) the front-end (non-certified) and (2) the
back-end (certified). The front-end parses the SMT file, whichCPP ’22, January 17–18, 2022, Philadelphia, PA, USA

Shuanglong Kan, Anthony W. Lin, Philipp Rümmer, and Micha Schrader

CertiStr
Front-end:
RE to NFA

SMT file(str-constraints)

Results:
Back-end:
Forward-propagation

SMT to IDS

Automata LibraryNon-certified

certifiedsat
unknown
unsat

Figure 1. The framework of the certified string solver
will first translate all Regular Expressions (RE) to NFAs anddesugar some string constraints that are not in the fragment,
and then translate the string constraints to the Intermediate
Data Structures (IDS), which are the inputs of the back-end.
The IDS contains three parts: (1) a set S of variables that areused in the string constraints, (2) a concatenation constraint
map Concat, which maps variables in S to the set of theirconcatenation constraints, and (3) a regular constraint map
Reg, which maps each variable in S to its regular membership
constraints.
The back-end contains two parts: (1) the Automata Library,which contains a collection of automata operations, suchas the product and concatenation of two NFAs, and (2) aforward-propagation to check whether the string constraints
are satisfiable. The results of the certified string solver canbe (1) sat the string constraint is satisfiable, (2) unsat thestring constraint is unsatisfiable, and (3) unknown the solver
cannot decide whether the string constraint is satisfiable
or not. Note that, unknown does not mean that CertiStr is
non-terminating. It means the results after executing theforward-propagation for string constraints are not sufficient
to decide their satisfiability.

4

Forward-propagation of String
Constraints

In this section, we present the algorithm of the forwardpropagation and the properties proven for it.
4.1

The Algorithm of Forward-propagation

We use the following example of string constraints to illustrate our forward-propagation analysis.
Example 4.1. x 1 ∈ A1 ∧ x 2 ∈ A2 ∧ x 3 ∈ A3 ∧ x 5 = x 3 +x4 ∧ x3 = x1 + x2.
x5

x3

x1

x4

x2

Figure 2. Dependence graph of variables in Example 4.1

Example 4.1 contains five variables “x 1 , x 2 , x 3 , x 4 , x 5 ” andtwo concatenation constraints “x 5 = x 3 +x 4 ∧x 3 = x 1 +x 2 ”. We
can view these concatenation constraints as a dependence
graph shown in Figure 2. For a concatenation constraint
x k = x i + x j , it yields two dependence relations: x k 7→ x iand x k 7→ x j (a 7→ b denotes a depends on b). This meansthat before propagating the concatenation of the regularconstraints of x i and x j to x k , we need to first compute thepropagation to x i and x j . Let the initial regular constraintof x k be Ak . Let the regular constraints of x i and x j be
Ai and A j , respectively. The new regular constraint of x k
after the propagation can be refined to an automaton, whose
language is L(Ak ) ∩ (L(Ai ) + L(A j )), where L1 + L2 ≜{w 1w 2 | w 1 ∈ L1 ∧ w 2 ∈ L2 }. Here, the term “refine" means
narrowing the regular constraint of a variable by propagating
the concatenation constraints.
The forward-propagation repeats the following computation until all variables are refined:• detect a set of variables such that for each variable inthe set, all its dependence variables have already beenrefined.
• refine the regular constraints of the variables detectedin the last step with respect to their concatenation
constraints.
We illustrate the idea of the forward-propagation with
Example 4.1. The first iteration of the forward-propagation
will detect the set of variables {x 1 , x 2 , x 4 } since they haveno dependence variables and we do not need to refine theirregular constraints. The second iteration of the forwardpropagation will detect the set of variables: {x 3 }, as x 3 only
depends on the variables in {x 1 , x 2 , x 4 }. Its regular constraint
will be refined to an automaton, whose language is L(A3 ) ∩(L(A1 ) + L(A2 )) after the propagation for the constraint
x 3 = x 1 + x 2 . Assume this new regular constraint as A3′ .
The third iteration detects the variable x 5 , whose regularconstraint will be refined to an automaton, whose languageis Σ∗ ∩ (L(A3′ ) + Σ∗ ). Note that we do not specify the initial
regular constraints of x 4 and x 5 in the string constraint andtherefore their initial regular constraints are Σ∗ by default.
Algorithm 1 shows the forward-propagation algorithm. It
contains three procedures: Forward_Prop, Ready_Set, and
Var_Lang. The procedure Forward_Prop is the entry pointof the algorithm and has three parameters: (1) S is the set

CertiStr: A Certified String Solver

Algorithm 1 The algorithm of forward-propagation
1: procedure Forward_Prop(S, Concat, Reg)
2:
R←∅
3:
while S , ∅ do

4:
C ← Ready_Set(S, Concat, R)
5:Reg ← Var_Lang(C, Concat, Reg)6:S ← S − C; R ← R ∪ C
7:
end while
8:
return Reg
9: end procedure

10: procedure Var_Lang(C, Concat, Reg)11:
for each v ∈ C do
12:
A ← (Reg v)
13:for each (v 1 , v 2 ) ∈ (Concat v) do
14:
A ′ ← NFA_concat (Reg v 1 ) (Reg v 2 )15:
A ← NFA_product A A ′16:
end for17:
Reg ← Reg [v 7→ A]
18:
end for19:
return Reg
20: end procedure
22: procedure Ready_Set(S, Concat, R)
23:
C←∅
24:
for each v ∈ S do

D←∅
for each (v 1 , v 2 ) ∈ (Concat v) doD ← D ∪ {v 1 , v 2 }end forif D ⊆ R thenC ← C ∪ {v}31:
end if32:
end for33:
return C
34: end procedure

25:
26:
27:
28:
29:
30:

of variables used in the string constraints, for instance, in
Example 4.1, there are five variables: S = {x 1 , x 2 , x 3 , x 4 , x 5 };(2) Concat : S ⇀ 2 (S ×S ) is a partial map which maps avariable x to a set of pairs of variables. For each pair (x 1 , x 2 )in the set, there is a concatenation constraint: x = x 1 + x 2 ;(3) Reg : S → N is a map from variables to automata. These
automata denote the variables’ initial regular constraints.
Here N denotes the set of NFAs.
In the while loop of the procedure Forward_Prop, thecomputation iteratively refines the regular constraints ofvariables by propagating the regular constraints of variableson the right hand side of the concatenation constraints. The
first step in the loop computes the set C of variables whose
dependence variables are all in the set R (computed by theprocedure Ready_Set), R is initialized empty and it denotes
the set of variables that have already been refined by the previous loops. The second step in the loop updates the regular

CPP ’22, January 17–18, 2022, Philadelphia, PA, USA

constraints of the variables in C stored in Reg by propagating the concatenation constraints in Concat (computed by
Var_Lang).
At the end of the loop body, the set S is updated by removing the variables in C as they have already been refined
and these removed variables are added to the set R, i.e., they
have already been refined.
The procedure Ready_Set computes the set of variables
that are only dependent on the variables in R. For each variable v, it stores all its dependence variables in D and thenchecks whether D is a subset of R. If D is a subset of R thenv is moved to C as all its dependence variables have beenrefined.
The procedure Var_Lang refines the regular constraintsof variables in C. In the inner loop of Var_Lang, it traverses
all concatenation constraints v = v 1 + v 2 and refines theregular constraint of v by propagating the concatenation of
the regular constraints of v 1 and v 2 . Reg [v 7→ A] means
updating the regular constraint of v in Reg to A. The functions NFA_concat and NFA_product denote constructing
the concatenation and product of two NFAs, respectively.
These two functions will be introduced in Section 5.
Assume a string constraint is stored in S, Concat and Reg,then after calling “Forward_Prop(S, Concat, Reg)”, we will
get a new Reg ′ such that for each variable v, (Reg ′ v) storesthe refined regular constraint of v, which is an NFA. We
have two cases to decide whether the string constraint issatisfiable or not:• If there exists a variable v such that the language of(Reg ′ v) is empty then the string constraint is unsatisfiable, because the refined regular constraint of v isthe empty language.
• If for all variables v such that the language of (Reg ′ v)
is not empty then unfortunately we cannot decide
whether the string constraint is satisfiable or not. Consider the string constraint: “(1) y = x + x ∧ (2) y ∈{ab} ∧ (3) x ∈ {a, b}”, where ab, a, and b are words,
the refined regular constraints of x and y are both not
empty. But this string constraint is not satisfiable asconstraints (1) and (2) require x to have two different values. We will introduce a property, called tree
property later, such that if the string constraint satisfies the tree property then it is satisfiable, otherwise
CertiStr returns unknown.
4.2

Theorems for Forward-propagation

Now we introduce the key theorem proven for the algorithm.
Firstly we present the definitions of well-formed inputs (wfin Figure 3) and the acyclic property (acyclic in Figure 3)
for concatenation constraints, which are the premises of thecorrectness theorem.
The wf predicate requires that all variables appearing in
the domain and codomain of Concat should be in the set

CPP ’22, January 17–18, 2022, Philadelphia, PA, USA

Shuanglong Kan, Anthony W. Lin, Philipp Rümmer, and Micha Schrader

definition wf where
wf S Concat Reg =(dom Concat ⊆ S)∧(dom Reg = S)∧(∀ v v 1 v 2 . v ∈(dom Concat) ∧ (v 1 , v 2 ) ∈ (Concat v)−→ v 1 ∈ S ∧ v 2 ∈ S ) ∧ finite S

Now we are ready to introduce our correctness theorem(Theorem 4.2). The keyword fixes in Isabelle is used to define
universally quantified variables. The keyword assumes isused to specify assumptions of the theorem and the keyword shows is used to specify the conclusion of the theorem. The shows part is of the form ”M ≤ SPEC (λ Reд ′ . Φ)”,which means the algorithm M is correct with respect tothe specification Φ. More precisely, the result of applying
the predicate (λ Reд ′ . Φ) to the output of M should be true.
“NFA_accept w A” checks whether w is accepted by A,
which will be introduced in Section 5. The symbol “@” isthe list concatenation operation in Isabelle. We use a list ofelements in Σ to represent a word.

definition acyclic whereS
acyclic S Concat l = S = (set l ) ∧ ((l = [])S∨(l = s#l ′ −→ (s ∩ ( (set l ′ )) = ∅) ∧(∀v 1 v 2 v. v ∈ s ∧ (v 1 , v 2 ) ∈ (Concat v) −→S{v 1 , v 2 } ⊆ (set l ′ ))∧(acyclic (S − s) Concat l ′ )))Figure 3. The definitions of wf and acyclic

S, and the domain of Reg should be the set S, i.e., all variables should have their initial regular constraints. S should
be finite. Now we consider the definition of acyclic, whichchecks whether the dependence graphs of concatenation
constraints are acyclic. Forward_Prop cannot solve string
constraints that are not acyclic. For instance, the string constraint “x = y1 +y2 ∧y1 = z 1 + x” does not satisfy the acyclic
property, as x 7→ y1 7→ x.
In order to specify the acyclic property, we arrange theset S of variables to a list in which elements are disjoint
sets of variables in S and the list characterizes the dependence levels among variables. For instance, in Example 4.1,
there are 5 variables and they can be organized in a list:[{v 5 }, {v 3 }, {v 1 , v 2 , v 4 }]. Indeed, the list characterizes the dependence levels among variables. For instance, the variablev 5 only depends on the variables in {v 3 } and {v 1 , v 2 , v 4 } andv 3 only depends on the variables in {v 1 , v 2 , v 4 } but not {v 5 }.
The variables in {v 1 , v 2 , v 4 } do not depend on any variables.
If Concat does not satisfies the acyclic property then we cannot arrange all variables in such a list, as all variables in acycle always depend on another variable in the cycle.
S
The predicate acyclic contains two parts. (1) S = (set l ),which means the elements in S and l should be exactly thesame. “set l” translates the list l to a set of elements in l andS“ (set l ) = {x | ∃y.y ∈ set l ∧ x ∈ y}”. (2) Part 2 further has
two cases. The first case is “l = []”, i.e., empty list. In this case,the predicate is obviously true. The second case is “l = s#l ′”,i.e., it has at least one element. s is the first element and l ′ isthe tail. In this case, firstly, it requires the elements in s to be
disjoint with the elements in the sets of the tail l ′ (checked bySs ∩ ( (set l ′ )) = ∅). Secondly, let v be a variable in s, for any
two variables v 1 and v 2 that v depends on, v 1 and v 2 can only
be in the sets of the tail l ′. Thirdly, acyclic (S − s) Concat l ′checks whether the remaining elements in S − s are still
acyclic w.r.t. Concat and l ′. In order to check whether thevariables in S are acyclic w.r.t. Concat, we can specify it as“∃l . acyclic S Concat l”.

Theorem 4.2 (Correctness of Forward_Prop).
fixes S Concat Reg
assumes 1. wf S Concat Reg
2. (∃l . acyclic S Concat l )shows Forward_Prop(S, Concat, Reg) ≤ SPEC (λReg ′ .
(∀v w. NFA_accept w (Reg ′ v) ←→(NFA_accept w (Reg v) ∧(∀v 1 v 2 . (v 1 , v 2 ) ∈ (Concat v) −→(∃w 1 w 2 . w = w 1 @w 2 ∧NFA_accept w 1 (Reg ′ v 1 )∧NFA_accept w 2 (Reg ′ v 2 ))))))
Theorem 4.2 shows that if S, Concat, Reg are well-formed
and acyclic then after calling Forward_Prop(S, Concat, Reg)
we can get Reg ′, which satisfies: any w is accepted by theautomaton (Reg ′ v) if and only if
1. w is accepted by the original regular constraint of v,i.e., (Reg v), and
2. for all variables v 1 and v 2 , (v 1 , v 2 ) ∈ Concat v implies
there exist w 1 , w 2 such that w = w 1 @w 2 and w i , fori = 1, 2, is accepted by the regular constraint (Reg ′ vi ).
That is, in the new Reg ′, the concatenation constraints areused to refine the corresponding variables.
Moreover, in Isabelle, Theorem 4.2 also requires us toprove the termination of Algorithm 1. The termination isproven by showing that in the procedure Forward_Prop, thenumber of variables in S decreases progressively for each
iteration. Since S is finite, the algorithm must terminate.
Even though Theorem 4.2 is the key of the correctness ofthe forward-propagation, it does not give us an intuition withrespect to the satisfiability semantics of string constraints
introduced in Section 3. In the following, we will show that
our forward-propagation is sound w.r.t. unsat results.
Firstly we need to formalize the semantics of sat and unsat
for string constraints. Let µ be an assignment, which is a map
S → Σ∗ from variables in S to words. We define the predicate
sat_str in Figure 4 for the semantics of the satisfiability ofstring constraints.
The predicate sat_str contains two parts: (1) the assignment µ should respect all regular constraints and (2) the
assignment µ should respect all concatenation constraints.

CertiStr: A Certified String Solver

definition sat_str where
sat_str S Concat Reg µ =(∀v ∈ S. (µ v) ∈ L(Reg v))∧(∀v v 1 v 2 . v ∈ S ∧ (v 1 , v 2 ) ∈ (Concat v) −→(µ v) = (µ v 1 )@(µ v 2 ))definition tree wheretree Concat =(∀v v 1 v 2 . (v 1 , v 2 ) ∈ Concat v −→ v 1 , v 2 ) ∧(∀v v 1 v 2 v 3 v 4 . (v 1 , v 2 ) , (v 3 , v 4 ) ∧(v 1 , v 2 ) ∈ Concat v ∧ (v 3 , v 4 ) ∈ Concat v−→ {v 1 , v 2 } ∩ {v 3 , v 4 } = ∅) ∧(∀v v ′ v 1 v 2 v 3 v 4 . v , v ′ ∧ (v 1 , v 2 ) ∈ Concat v∧(v 3 , v 4 ) ∈ Concat v ′ −→ {v 1 , v 2 } ∩ {v 3 , v 4 } = ∅)Figure 4. The definitions of sat_str and tree

Theorem 4.3 shows that after executing Forward_Prop,
we get a new map Reg ′. If there exists a variable v, suchthat L(Reg ′ v) = ∅, i.e., the language of the refined regularconstraint of v is the empty set, then there is no assignmentµ that makes the predicate “sat_str S Concat Reg µ” true.
Theorem 4.3 (Soundness for unsat results).
fixes S Concat Reg
assumes 1. wf S Concat Reg)2. (∃l . acyclic S Concat l )shows Forward_Prop(S, Concat, Reg) ≤ SPEC (λ Reg ′ .
((∃v. L(Reg ′ v) = ∅) −→(∀µ. ¬ sat_str S Concat Reg µ)))Unfortunately, the theorem holds only for unsat results.
As we already analyzed before, the case ∀v. L(Reg ′ v) , ∅cannot make us conclude that the string constraint is satisfiable.
In this paper, we characterize a subset of the string constraints, using a property such that the forward-propagation’s
satisfiable results are also sound. We call it the tree property.
The intuition behind the tree property is that the dependence
graph of a string constraint should constitute a tree or forest.
The example y = x + x does not satisfy the tree property,
because y has two edges pointing to a same node x in thedependence graph. In other words, the node x has indegree 2.
But a tree requires that each node has at most indegree 1. As
the map Concat stores the dependence graphs of string constraints, we only need to check Concat for the tree property.
The predicate tree is defined in Figure 4.
This definition has three cases separated by the conjunction operator: (1) the first case requires that for any concatenation constraint v = v 1 + v 2 , we have v 1 , v 2 . (2) The
second case requires that for any variable v with two concatenations v = v 1 + v 2 and v = v 3 + v 4 , {v 1 , v 2 } and {v 3 , v 4 }CPP ’22, January 17–18, 2022, Philadelphia, PA, USA

are disjoint. (3) The third case requires that for any two different variables v and v ′ with the concatenation constraintsv = v 1 +v 2 and v ′ = v 3 +v 4 , {v 1 , v 2 } and {v 3 , v 4 } are disjoint.
With this definition we have the following theorem.
Theorem 4.4 (Completeness for the tree property).
fixes S Concat Reg
assumes 1. wf S Concat Reg
2. (∃l . acyclic S Concat l )3. tree Concat
shows Forward_Prop(S, Concat, Reg) ≤ SPEC (λ Reg ′ .
((∀v. L(Reg ′ v) , ∅) ←→(∃µ. sat_str S Concat Reg µ)))This theorem shows that if Concat satisfies the tree property then we have: Reg ′ satisfies that for all v, the languageof Reg ′ v is not empty iff there exists an assignment, whichmakes the string constraint satisfiable.
In order to check whether a string constraint satisfies thetree property, we propose Algorithm 2. It first stores all thevariables, which are on the right hand side of the concatenation constraints, into a list, and then checks whether the list
is distinct. If it is not distinct then there must exist a variablewith at least indegree 2 and thus Concat cannot satisfy thetree property.
Algorithm 2 Tree property checking
1: procedure Check_Tree(S, Concat)2:l ← []

for each v ∈ S dofor each (v 1 , v 2 ) ∈ (Concat v) dol ← v1 # v2 # l
end forend for8:
return distinct l
9: end procedure
3:
4:
5:
6:
7:

Now we show that if Algorithm 2 returns True then thetree property is satisfied.
Theorem 4.5 (Correctness of Check_Tree).
fixes S Concat
assumes 1. dom Concat ⊆ S
2. (∀v v 1 v 2 .(v 1 , v 2 ) ∈ Concat v −→ {v 1 , v 2 } ⊆ S )shows Check_Tree(S, Concat) −→ tree Concat
With the function Check_Tree, CertiStr can return three
results: unsat, sat, and unknown, in which unknown means
the string constraint does not satisfy the tree property andthe forward-propagation does not refine the regular constraint of any variable to empty.
We now finish introducing the forward-propagation procedure. As it uses many NFA operations, in the following
section, we will introduce our implementation for these NFA
operations.

CPP ’22, January 17–18, 2022, Philadelphia, PA, USA

Shuanglong Kan, Anthony W. Lin, Philipp Rümmer, and Micha Schrader

5

record NFA = Q :: " 'q set "∆ :: "( ' q *' a set * 'q ) set "I :: " 'q set "F :: " 'q set "Symbolic Automata Formalization

Automata operations are the key to our certified string solver.
For instance, we need to check the language emptiness ofan NFA as well as construct the concatenation and productof two NFAs. In order to make the string solver practicallyuseful, we should also keep the efficiency in mind.
As argued by D’Antoni et. al [15], the classical definition
of NFA, whose transition labels are a character in the alphabet, is not suitable for practical implementation, and they
propose s-NFAs, which allow transition labels to carry a setof characters, to address this limitation. In this section, we
present our formalization of s-NFAs in Isabelle.
Definition 5.1 (Abstract s-NFAs). An s-NFA is a 5-tuple:
A = (Q, Σ, ∆, I , F ), where Q is a finite set of states, Σ is analphabet (Σ may be infinite), ∆ ⊆ Q × 2Σ × Q is a finite set oftransition relations, I ⊆ Q is a set of initial states, and F ⊆ Q
is a set of of accepting states.
For a transition (q, α, q ′ ) in an s-NFA, the implementation of α can use various different data structures, such as
intervals for string solvers and Binary Decision Diagrams(BDD) for symbolic model checkers. Definition 5.1 of s-NFAs
is called abstract s-NFAs because the transition labels aredenoted as sets instead of using concrete data structures, likeintervals and BDDs.
In order to make our formalization of s-NFAs reusable fordifferent implementation of transition labels, we exploit Isabelle’s refinement framework and divide the formalizationof s-NFAs in two levels: (1) the abstract level (introduced inthis section) and (2) the implementation level (introducedin the following section). When the correctness of the algorithms at the abstract level is proven, the implementationlevel does not need to re-prove it, only the refinement relations between these two levels must be shown.
At the abstract level, transition labels are modeled as a
set as shown in Definition 5.1. At the implementation level,
the sets of characters are refined to concrete data structures,such as intervals or BDDs.
Our formalization of s-NFAs extends an existing classicalNFA formalization developed by Tuerk et al. [40]; this formalization is part of the verified CAVA model checker [26].
We extend it to support s-NFAs and further operations, suchas the concatenation operation of two NFAs. Figure 5 shows
the Isabelle formalization of s-NFAs. An s-NFA is defined bya record with four elements: (1) Q is the set of states, (2) I is
the set of initial states, (3) F is the set of accepting states, and(4) ∆ is the set of transitions with transition labels definedby sets. The definition well-formed is a predicate to check
whether an NFA satisfies (1) the states occurring in the setsof initial and accepting states are also in the set (Q A) of
states. In Isabelle, the value of a field fd in a record rd can beextracted by (fd rd). Therefore, (Q A) denotes the value ofthe field Q in A. (2) The states in the set of transitions should
also be in (Q A). (3) (Q A) is a finite set. (4) ∆ is finite.

definition well-formed where
well-formed A = (I A) ⊆ (Q A) ∧ (F A) ⊆ (Q A)∧ finite (Q A) ∧ finite ∆ ∧(∀(q, α, q ′ ) ∈ ∆, q ∈ (Q A) ∧ q ′ ∈ (Q A))
fun reachable w ∆ q q ' wherereachable [] ∆ q q ' = ( q =q ')| reachable ( a # w ) ∆ q q ' =(∃qi α . (q ,α ,qi )∈∆∧ a∈ α ∧ reachable w ∆ qi q ')definition NFA_accept where
NFA_accept w A = (∃q q ′ . q ∈ (I A) ∧ q ′ ∈ (F A)∧ reachable w (∆ A) q q’)
definition L where
L A = {w. accept w A}
Figure 5. Isabelle formalization of abstract symbolic NFA

For a word w = a 1a 2 . . . an and two states q and q’, thefunction reachable checks whether there exists a path q 0 , α 1 ,q 1 , . . . , qn−1 , α n , qn in the NFA A such that q = q 0 ∧ q’ = qn ,(qi−1 , α i , qi ) ∈ (∆ A), 1 ≤ i ≤ n and a j ∈ α j , 1 ≤ j ≤ n. The
definition NFA_accept checks whether a word is acceptedby an NFA and the definition of L is the language of an NFA.
Based on this definition of NFAs, a collection of automata
operations are defined and their correctness lemmas areproven. Here we only present the operation of the concatenation shown in Figure 6.
NFA_concat_basic constructs the concatenation of two
NFAs. The correctness of this definition relies on the factthat the sets of states in the two NFAs are disjoint. In thedefinition of NFA_concat_basic, the set of transitions of theconcatenation is the union of (1) (∆ A1 ), (2) (∆ A2 ), and (3){(q, α, q ′′ ) | ∃q ′ .(q, α, q ′ ) ∈ (∆ A1 ) ∧ q ′ ∈ (F A1 ) ∧ q ′′ ∈(I A2 )}. The transitions in (3) concatenate the language of
A1 to the language of A2 .
The set of the initial states in the concatenation is computed by first checking whether there is a state that is inboth the sets of initial and accepting states of A1 . If there
exists such a state then the initial states in the concatenation
should include the initial states of A2 , as A1 accepts theempty word, otherwise the initial states of the concatenation
are A1 ’s initial states.

CertiStr: A Certified String Solver

definition NFA_concat_basic where
NFA_concat_basic A1 A2 ≡ L
Q = ( Q A1 ) ∪ ( Q A2 ) ,∆ = (∆ A1 ) ∪ (∆ A2 ) ∪{(q, α, q ′′ ) | ∃q ′ .(q, α, q ′ ) ∈ (∆ A1 )∧q ′ ∈ (F A1 ) ∧ q ′′ ∈ (I A2 )},I = if (( I A1 ) ∩ ( F A1 ) = ∅) then ( I A1 )else (( I A1 ) ∪ ( I A2 )) ,F = ( F A2 )M
definition NFA_concat where
NFA_concat A1 A2 f 1 f 2 =remove_unreachable_states(NFA_concat_basic(NFA_rename f 1 A1 )(NFA_rename f 2 A2 ))Figure 6. The definition of concatenation operation

The definition of NFA_concat firstly renames the statesin both NFAs to ensure their sets of states disjoint. In theterm “NFA_rename f A”, f is a renaming function, for instance, f can be “λq.(q, 1)”, which renames any state q to(q, 1). “NFA_rename f A” renames all states in (Q A) by thefunction f . Correspondingly, all states in transitions, initialstates, and accepting states are also renamed by f . Renaming
states makes it easier to ensure the sets of states of two NFAs
are disjoint. The function remove_unreachable_states removes all states in an NFA that are not reachable from theinitial states of the NFA. This enables us to check the language emptiness of an NFA by only checking the emptinessof its set of accepting states. At the implementation level,
the algorithm also only generates reachable states for NFAs.
But with remove_unreachable_states used in NFA_concat
at the abstract level, the refinement relation between these
two levels can be specified as the NFA isomorphism of thetwo output concatenations of automata at the two levels,
instead of language equivalence, which is more challenge toprove.
In order to ensure the correctness of this operation, we
need to prove the following lemma in Isabelle.
Lemma 5.2 (Correctness of NFA_concat).
fixes A1 A2 f 1 f 2
assumes 1. well-formed A1
2. well-formed A2
3. (image f 1 (Q A1 )) ∩ (image f 2 (Q A2 )) = ∅4. inj_on f 1 (Q A1 )∧ inj_on f 2 (Q A2 )shows L(NFA_concat A1 A2 f 1 f 2 ) ={w 1 @w 2 . w 1 ∈ L(A1 ) ∧ w 2 ∈ L(A2 )}CPP ’22, January 17–18, 2022, Philadelphia, PA, USA

The assumptions well-formed A1 and well-formed A2
require the input NFAs to be well-formed. In addition, the assumption (image f 1 (Q A1 )) ∩ (image f 2 (Q A2 ))= ∅ requiresthat after renaming the states in both A1 and A2 , the newsets of states of the two NFAs are disjoint. The term “image
f S” applies the function f to the elements in the set S andreturns a new set { f e. e ∈ S }. The premises inj_on f 1 (Q A1 )and inj_on f 2 (Q A2 ) require that the functions f 1 and f 2
are injective over the sets (Q A1 ) and (Q A2 ), respectively.
The conclusion in “shows” specifies that the language ofthe concatenation of A1 and A2 is exactly the set of theconcatenations of the words in A1 and the words in A2 ,Moreover, some other important functions are defined, forinstance:• The product of two NFAs: NFA_product A1 A2 , which
computes the product of A1 and A2 . Its correctness
theorem is L(NFA_product A1 A2 ) = L(A1 )∩L(A2 ).
• Checking the isomorphism of two NFAs:
NFA_isomorphism A1 A2 ≜ (∃f .inj_on f (Q A1 ) ∧NFA_rename f A1 = A2 ). Some lemmas are provenfor it, such as, well-formed A1 ∧ well-formed A2 ∧NFA_isomorphism A1 A2 −→ L(A1 ) = L(A2 ).
Section 4 and this section present the abstract level algorithms for the forward-propagation and the NFA operations,
respectively. In order to make CertiStr efficient and practically useful, we need to use some efficiently implemented
data structures, such as red-black-trees (RBT) and hash maps.
This will be introduced in the following section.

6

Implementation-Level Algorithms

In this section, we will first present the relations between abstract concepts, like sets and maps, and the implementation
data structures in Isabelle (Subsection 6.1), which is the prerequisite to understand the implementation-level algorithm
in Subsection 6.2.
6.1

Isabelle Collections Framework

Isabelle Collections Framework (ICF) [27] provides an efficient, extensible, and machine checked collections framework. The framework features the use of data refinement
techniques [25] to refine an abstract specification (using highlevel concepts like sets) to a more concrete implementation(using collection data structures, like RBT and hashmaps).
The code-generator of Isabelle can be used to generate efficient code.
The concrete data structures implement a collection ofinterfaces that mimic the operations of abstract concepts. We
list the following RBT implementation of set interfaces thatwill be used to present the implementation-level algorithms:• RBT .empty, generates an RBT representation of theempty set.
• RBT .mem e D, checks whether the element e is in theset represented by RBT D.

CPP ’22, January 17–18, 2022, Philadelphia, PA, USA

Shuanglong Kan, Anthony W. Lin, Philipp Rümmer, and Micha Schrader

record NFA_rbt =Q :: " ' q RBT "∆ :: "( ' q * 'a Interval * 'q ) RBT "I :: " ' q RBT "F :: " ' q RBT "In order to support NFA operation implementation, some
operations for intervals are implemented. We list the following 3 interval operations here.
• intersectionI [I 1 , I 2 ] [I 1′, I 2′ ] ≜ [max(I 1 , I 1′ ), min(I 2 , I 2′ )],the intersection of two intervals. The term max(I 1 , I 1′ )returns the bigger one of I 1 and I 1′ , and min(I 2 , I 2′ ) returns the smaller one of I 2 and I 2′
• nemptyI [I 1 , I 2 ] ≜ I 1 ≤ I 2 , checking the non-emptinessof the interval [I 1 , I 2 ].
• memI e [l 1 , l 2 ] ≜ l 1 ≤ e ≤ l 2 , checking the membership of an element e and the interval [l 1 , l 2 ].

Figure 7. NFA data structure definition using RBT• RBT .insert e D, inserts the element e into the set represented by RBT D.
• RBT .inter D 1 D 2 , computes the RBT representation of
the set intersection of D 1 and D 2 . D 1 and D 2 are both
RBT represented sets.
• RBT .union D 1 D 2 , computes the RBT representationof the set union of D 1 and D 2 . D 1 and D 2 are both RBT
represented sets.
• RBT .iterator D v f , where f is of the type t 1 ⇒ t 2 ⇒t 2 , v is of the type t 2 , and the elements in D are of
the type t 1 . This interface implementation iteratively
applies the function f to the elements in D with theinitial value v. For instance, the first iteration of thecomputation of “RBT .iterator {e 1 , e 2 } v f ” selects anelement from {e 1 , e 2 }, assume e 1 is selected, and thenapplies f to e 1 and v, i.e., f e 1 v. Assume the valueof “f e 1 v” is v ′. The second iteration applies f toe 2 and v ′. Now all elements in the set are traversed,“RBT .iterator {e 1 , e 2 } v f ” finishes with the return valueof “f e 2 v ′”.
• RBT .to_list D translates a set represented by D to alist.
• RBT .α D translates RBT represented set D to the set
in the abstract concept.
6.2

Implementation-Level Algorithm for
NFA_concat

In this subsection, we present the implementation-level algorithm by the NFA operation NFA_concat.
In order to formalize implementation-level algorithms, thefirst step is to consider the data refinement. At the abstractlevel, we use sets to store states, transitions, initial states,
and accepting states. At the implementation level, we use
RBTs to replace sets to store these elements of NFAs. The
type of NFAs using RBT data structures is specified in Figure
7. Note that, here we only give a simplified version of the
RBT NFA definition to make it easy to understand. Indeed,
RBT has more type arguments.
Moreover, for each transition (q, α, q ′ ), the label α is represented by a set at the abstract level. We use intervals to
replace sets to store α. An interval [n 1 , n 2 ] is a pair of elements in a totally ordered set. The semantics of an interval
is defined by a set as semI [n 1 , n 2 ] = {n | n 1 ≤ n ≤ n 2 }.

Algorithm 3 The algorithm idea of NFA concatenation
1: procedure Construct_Trans(S ∆1 , S ∆2 , S I 2 , S F 1 )S D ← RBT .union S ∆1 S ∆2 ;RBT .iterator S ∆1 S D(λ(q, a, q ′′ ) S.
if (RBT .mem q ′′ S F 1 ) then
RBT .iterator S I 2 S(λq ′ S ′ . RBT .insert (q, a, q ′ ) S ′)8:
end if);9:
return S D ;10: end procedure
2:
3:
4:
5:
6:
7:

11:
12: procedure NFA_Concate_Impl(A 1 , A 2 , f 1 , f 2 )13:▷ A1 , A2 are of type NFA_rbt

A1′ ← NFA_Rename_Impl f 1 A1 ;A2′ ← NFA_Rename_Impl f 2 A2 ;if RBT .inter (I A1′ ) (F A1′ ) , RBT .empty thenS I ← RBT .union (I A1′ ) (I A2′ )else
19:
S I ← (I A1′ )20:
end if;
21:
SQ ← S I ; S ∆ ← RBT .empty; wl ← RBT .to_list SQ ;22:
S ∆′ ← Construct_Trans(∆ A1′ , ∆ A2′ , I A2′ , F A1′ );23:while wl , [] do▷ “[]” denotes empty list24:
qs ← wl .rm_first ;25:▷ “rm_first”: removes and returns the first26:
element in wl
27:
RBT .iterator S ∆′ S ∆28:(λ(q, α, q ′ ) S.
29:
if q = qs ∧ (nemptyI α ) then30:
if ¬(RBT .mem q ′ SQ ) then31:
RBT .insert q ′ SQ ;32:
wl ← wl@[q ′];33:
end if;34:
RBT .insert (q, α, q ′ ) S;
35:
end if;36:)
37:
end while38:
return (SQ , S ∆ , S I , RBT .inter SQ (F A2′ ))39: end procedure

14:
15:
16:
17:
18:

CertiStr: A Certified String Solver

definition NFA_α where
NFA_α A ≡ L Q = RBT .α ( Q A ) ,∆ = (image (λ(q, α, q ′ ).(q, semI α, q ′ ))(RBT .α (∆ A ))) ,I = RBT .α ( I A ) ,F = RBT .α ( F A )M
definition refine_rel whererefine_rel A A ′ =NFA_isomorphism (NFA_α A ′ ) A
lemma refine_rel_lang :well-formed A ∧ refine_rel A A ′=⇒ L(A) = L(NFA_α A ′ )Figure 8. Refinement relation formalization

Algorithm 3 shows the basic idea of the NFA_concat implementation (the procedure NFA_Concat_Impl). The texts
after “▷” are comments. NFA_Rename_Impl is the implementation of the NFA renaming function NFA_Rename at
the abstract level.
The sub-procedure Construct_Trans generates the set oftransitions for the concatenation of the two automata, whichcontains the transitions in both (∆ A1 ) and (∆ A2 ), and thetransitions that concatenate the two automata (cf. Figure 6
for the abstract algorithm of the concatenation ).
In Algorithm 3, Line 16-20 computes the initial states of
the concatenation. Line 21 initializes SQ , S ∆ , and wl, where
SQ stores the states of the concatenation NFA, S ∆ stores thetransitions of the concatenation NFA, wl is a list to mimica queue that stores the states to be expanded. Line 23 to
37 is the while loop for expanding the reachable states andtransitions. Finally Line 38 returns the concatenation of the
two NFAs. This algorithm constructs the concatenation of
two NFAs with only reachable states, which means that we
can check the emptiness of the concatenation NFA by only
checking the emptiness of its set of accepting states.
In order to ensure the correctness of the implementation
for concatenation, we need to prove the refinement relation
between NFA_concat and NFA_Concate_Impl.
In Figure 8, we formalize the refinement relations between
the two NFAs at the abstract level and the implementationlevel. The function NFA_α translates an implementationlevel NFA A (its type is NFA_rbt) to an abstract-level NFAof the type NFA. The definition refine_rel defines the refinement relation between an abstract-level NFA A and an
implementation NFA A ′, which requires the isomorphism
between A and (NFA_α A ′ )Lemma 6.1 specifies that the concatenation implementation correctly refines the abstract concatenation definition.

CPP ’22, January 17–18, 2022, Philadelphia, PA, USA

Lemma 6.1 (Correctness of NFA_Concate_Impl).
fixes A1 , A2 , A1′ , A2′ , f 1 , f 2 , f 3 , f 4
assumes
1. refine_rel A1 A1′ ∧ refine_rel A2 A2′
2. inj_on f 1 (Q A1 ) ∧ inj_on f 2 (Q A2 )3. (image f 1 (Q A1 )) ∩ (image f 2 (Q A2 )) = ∅4. inj_on f 3 (RBT .α (Q A1′ )) ∧ inj_on f 4 (RBT .α (Q A2′ ))5. (image f 3 (RBT .α (Q A1′ ))) ∩ (image f 4 (RBT .α (QA2′ )))= ∅6. A = NFA_concat(A1 , A2 , f 1 , f 2 )7. A ′ = NFA_Concate_Impl(A1′ , A2′ , f 3 , f 4 )shows refine_rel A A ′This theorem shows that the implementation-level concatenation of two NFAs is a refinement for the concatenationof the corresponding abstract-level NFAs. With Lemma 6.1
and Lemma refine_rel_lang, we can easily infer that thelanguage of the concatenation at the abstract level is equal
to the language of the concatenation at the implementationlevel.
In this section, we presented the implementation of theconcatenation operation. This implementation uses intervals to store transition labels. Indeed, our formalization ofs-NFAs can be reused to implement s-NFAs using other data
structures, such as BDDs, bitvectors, and Boolean formulas, to store transition labels. The corresponding operations,such as intersectionI, nemptyI, and memI, for these data
structures need to be implemented at the implementationlevel.
Moreover, the forward-propagation algorithm and otherautomata operations also have their corresponding implementations and their refinement relations with the abstract
algorithms have been proven.

7

Evaluation and Development Efforts

The tool CertiStr (https://github.com/uuverifiers/ostrich/tree/
CertiStr) is developed in the Isabelle proof assistant (version2020) and one can extract executable OCaml code from theformalization in Isabelle. To obtain a complete solver, weadded a (non-certified) front-end for parsing SMT-LIB problems (Figure 1); this front-end is written in Scala, and mostly
borrowed from OSTRICH [13]. In this section, we evaluate
CertiStr against the Kaluza benchmark [35], the most commonly used benchmark to compare string solvers. Moreover,
we also elaborate the development efforts for CertiStr.
7.1

The Effectiveness and Efficiency

The Kaluza benchmark contains 47284 tests, among which
38043 tests (80.4%) are in the string constraint fragment ofCertiStr. CertiStr supports string constraints with word equations of concatenation, regular constraints, and monadic
length. The benchmark is classified into 4 groups according
to the results of the Kaluza string solver: (1) sat/small, (2)sat/big, (3) unsat/small, and (4) unsat/big.

CPP ’22, January 17–18, 2022, Philadelphia, PA, USA

Shuanglong Kan, Anthony W. Lin, Philipp Rümmer, and Micha Schrader

Table 1. Experimental results of the Kaluza benchmark

sat_small
sat_big
unsat_small
unsat_big
total

total tests sat
19634
19302
774
521
8775
7376
8860
2502
38043
29700

unknown
332
253
824
4880
6289

Note that the benchmark classification is not in all cases
accurate, in the sense that there are some files in unsat/big
and unsat/small that are satisfiable, owing to known incorrect results that were produced by the original Kaluza string
solver [28, 35].
We ran CertiStr over these 38043 tests on an AMD Opteron2220 SE machine, running 64-bit Linux and Java 1.8 (for running the Scala front-end of CertiStr). The results are shownin Table 1. The column “total tests” denotes the total numberof tests in a group. The columns “sat”, “unknown” , “unsat”
denote the numbers of tests for which CertiStr returns sat,
unknown, and unsat, respectively. The column "solved%" denotes the percentage of the tests for which the string solver
returns sat or unsat. The columns "avg.time(s)" and “timeout"
denote the average time for running each test in CertiStr andthe number of tests that time out, respectively. The column"CVC4" denotes the average execution time of the state of
the art string solver CVC4, which can efficiently solve all
the string constraints without timeout. The time limit forsolving each test is 60 seconds.
From Table 1, we can conclude that in total, 83.5% of thetests can be solved by CertiStr with the result sat or unsat.
The remaining of the tests are unknown or timeout. The
groups sat_small and unsat_small have the higher solved
percentages, more than 90%, compared with sat_big andunsat_big. This is easy to understand as small tests have ahigher probability to satisfy the tree property. The worst
group is unsat_big. CertiStr can solve 45% tests in this group.
The reason is that in this group, there are a lot of tests withmore than 100 concatenation constraints, which significantly
increases their probability of violating the tree property. For
the groups unsat_big and unsat_small, CertiStr detects 2502
and 7376 tests, respectively, that are indeed satisfiable.
Moreover, in unsat_big, there are 728 tests that time out.
After analyzing these tests, we found that a variable with a lotof concatenation constraints (i.e., the variable appears manytimes on the left-hand sides of the concatenation constraints)
can easily yield s-NFA state and transition explosion during
the forward-propagation. In order to evaluate such a state
explosion problem, we set a test of the form in Example 7.1:
Example 7.1.
x = x1 + x1 ∧ x = x2 + x2 ∧ x = x3 + x3 ∧ . . .

unsat
0
0
575
1478
2054

solved%
98.3%
67.3%
91%
45%
83.5%

avg. time(s)< 0.01
0.84
0.58
8.01
1.87

timeout
0
0
0
728
728

CVC4
< 0.010.04< 0.01
0.5
0.11

It is a test case with only the variable x on the left-handside. On the right-hand side, there are concatenations of theform xi + xi . No regular constraints are in the test.
We ran CertiStr over the test case by increasingly adding
more concatenations for the variable x. Table 2 shows theresults for solving the test case. Each column contains (1) the
number of concatenation constraints (No. Concat), (2) thesize of the automaton of the variable x after executing theforward-propagation (The numbers of states and transitionsof the automaton), and (3) the execution time for runningthe forward-propagation over the test (time).
From the table we can conclude that after adding 16 concatenation constraints for the variable x, the automaton generated for x contains 65536 states and 43046721 transitions.
Solving this test takes 168.28s.
Now consider the 728 tests that time out. These tests have
similar constraints, in which some variables have a lot of
concatenation constraints. During the forward-propagation,state and transition explosion happens for these tests, therefore they cannot be solved in 60s.
Compared with CVC4, which is not automata-based andincorporates more optimizations over its string theory decision procedure, CertiStr is less efficient. We can also optimize
CertiStr further in the future. For instance, we can optimize
the language intersection operation Σ∗ ∩ L(A) to L(A),and the language concatenation Σ∗ + Σ∗ to Σ∗ . We can also
implement NFA minimization algorithms to further improve
its efficiency. These optimizations can avoid the state explosion problem to some extent. However, integrating such
optimizations in a verified solver is challenging, as morecases need to be proven correct.
7.2

The Efforts of Developing CertiStr

In this subsection, we discuss the efforts of developing CertiStr.
Table 3 shows the efforts. The rows “Abs Automata Lib” and“Imp Automata Lib” denote abstract level and implementationlevel automata libraries, respectively. The rows "Abs Forward
Prop" and “Imp Forward Prop” denote abstract level and implementation level forward-propagations, respectively. The
column “Loc” denotes the lines of Isabelle code for each module. The column “Terms” denotes the number of definitions,functions, locales, and classes. The column “Theorems” denotes the number of theorems and lemmas in a module. The
development needs around one person-year efforts.

CertiStr: A Certified String Solver

CPP ’22, January 17–18, 2022, Philadelphia, PA, USA

Table 2. Experimental results for state and transition explosion
No. Concat
11
12
states 2048
4096
transitions 177147 531441
time (s)
0.43
1.29

13
8192
1594323
4.10

Table 3. Development effort of certified string solver
ModuleAbs Automata Lib
Imp Automata Lib
Abs Forward Prop
Imp Forward Prop
Total

Loc Terms
4484
100
8498
270
6850
37
2175
41
22007
448

Theorems
254
203
39
18
514

We now discuss the challenges in developing CertiStr.
The challenge in the automata library is the usage of sets
as transition labels. Classical NFAs require only the equality
comparison for transition labels. But for s-NFAs, we havemore operations for labels. For instance, we require the operations semI, intersectionI, nemptyI, memI for intervals.
These operations make it harder to prove the correctness of
the automata library.
The challenge in the forward-propagation module is theproofs of Theorem 4.2, 4.3, and 4.4. These theorems needaround 4000 lines of code to prove.

8

Related Works

String solvers. As introduced in Section 1, there already exist various non-certified string solvers, such as Kaluza [35],
CVC4 [28], Z3 [17], Z3-str3 [4, 5], Z3-Trau [9], S3P [39], OSTRICH [11–13], SLOTH [22], and Norn [1], among manyothers. These solvers are intricate and support more string
operations than CertiStr. Some of the solvers, such as Z3str3 and CVC4, opted to support more string operations andsettle with incomplete solvers (e.g. with no guarantee of termination) that could still solve many constraints that arise
in practice. Other solvers are designed with stronger theoretical guarantees; for instance, OSTRICH is complete for thestraight-line string constraint fragment [29]. CertiStr cansolve the string constraints that are out of the scope of thestraight-line fragment and guarantees to terminate for theconstraints without cyclic concatenation dependencies, but
it will return unknown for constraints that do not satisfy thetree property.
Symbolic Automata. CertiStr depends on automata operations for regular expression propagation and consistency
checking. An efficient implementation of automata is crucial. In comparison to finite-state automata in the classicalsense, symbolic automata [15, 16] have proven to be more
appropriate for applications like model checking, natural

14
16384
4782969
12.37

15
16
32768
65536
14348907 43046721
50.59
168.28language processing, and networking. Certified automata
libraries [7, 26] can provide trustworthiness for automatabased analysis in applications. However, to the best of ourknowledge, existing certified automata libraries are basedon the classical definition of automata, which makes theminefficient for practical applications with very large alphabets. Our work in this paper contributes to the developmentof certified symbolic automata libraries.
Paradigms toward certified constraint solvers. Two main
paradigms have emerged for the verification of constraint
solvers: (i) the verification of the solver itself, i.e., the development of solvers with machine-checked end-to-end correctness guarantees. For instance, Shi et al. [36] built a certified
SMT quantifier-free bit-vector solver. (ii) The generation ofcertificates, i.e., the actual solver is not verified, but its outputs are accompanied by proof witnesses that can then be
independently checked by a verified, trustworthy certificate
checker. For instance, Ekici et al. [19] provide an independent and certified checker for SAT and SMT proof witnesses.
In our work, we follow the first paradigm.
Security applications based on string analysis. There arevarious security applications of automata-based analysis andstring solvers, such as detecting web security vulnerabilities. Yu et al. [43] investigated the approach to use automata
theory for detecting security vulnerabilities, such as XSS, in
PHP programs. Their work also depends on a forward analysis. But the forward analysis is over the control flow graphsof PHP programs. CertiStr aims to build a stand-alone string
solver and the forward-propagation is only over the string
constraints. Many developments of string solvers, string analysis techniques, and automata-theoretic techniques were also
directly motivated by security vulnerability detection, e.g.,[2, 3, 10, 13, 22, 29, 35, 37–39]. To the best of our knowledge,
CertiStr is the first tool that provides certification of a string
analysis method that is applicable to security vulnerability
detection. We believe there is a need for further developmentof certified string analyzers: string solving techniques are
intricate and hence error-prone, but are applied for security
analysis whose correctness is of critical importance.

9

Conclusion and Future Works

In this paper, we present CertiStr, a certified string solver
for the theory of concatenation and regular constraints. The
backend of CertiStr is verified in Isabelle proof assistant,which provides a rigorous guarantee for the results of the

CPP ’22, January 17–18, 2022, Philadelphia, PA, USA

Shuanglong Kan, Anthony W. Lin, Philipp Rümmer, and Micha Schradersolver. We ran CertiStr over the benchmark Kaluza to show
the efficacy of CertiStr.
As future works, firstly, we plan to support more string
operations, such as string replacement and capture groups,
which are also widely used in programming languages, such
as JavaScript and PHP, increasing the applicability of CertiStr.
Secondly, the front end of CertiStr still needs to be verified
in Isabelle, especially the correctness of the desugaring fromstring constraints with monadic length functions and disjunctions to the language of CertiStr.

2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
UK, July 14-17, 2018, Proceedings, Part II (Lecture Notes in Computer
Science, Vol. 10982), Hana Chockler and Georg Weissenbacher (Eds.).
Springer, 45–51. https://doi.org/10.1007/978-3-319-96142-2_6[7] Julian Brunner. 2017. Transition Systems and Automata Isabelle
Library. Arch. Formal Proofs. https://www.isa-afp.org/entries/
Transition_Systems_and_Automata.html.
[8] Alexandra Bugariu and Peter Müller. 2020. Automatically testing
string solvers. In ICSE ’20: 42nd International Conference on Software
Engineering, Seoul, South Korea, 27 June - 19 July, 2020, Gregg Rothermel
and Doo-Hwan Bae (Eds.). ACM, 1459–1470. https://doi.org/10.1145/
3377811.3380398[9] Diep Bui and contributors. 2019. Z3-Trau. https://github.com/diepbp/
z3-trau.
[10] Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, and Zhilin
Wu. 2018. What is decidable about string constraints with the ReplaceAll function. Proc. ACM Program. Lang. 2, POPL (2018), 3:1–3:29.
https://doi.org/10.1145/3158091[11] Taolue Chen, Alejandro Flores-Lamas, Matthew Hague, Zhilei Han,
Denghang Hu, Shuanglong Kan, Anthony W. Lin, Philipp Ruemmer, and Zhilin Wu. 2022. Solving String Constraints with RegexDependent Functions through Transducers with Priorities and Variables. Proc. ACM Program. Lang. 6, POPL (2022).
[12] Taolue Chen, Matthew Hague, Jinlong He, Denghang Hu, Anthony Widjaja Lin, Philipp Rümmer, and Zhilin Wu. 2020. A Decision
Procedure for Path Feasibility of String Manipulating Programs with
Integer Data Type. In Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October
19-23, 2020, Proceedings. 325–342. https://doi.org/10.1007/978-3-03059152-6_18[13] Taolue Chen, Matthew Hague, Anthony W. Lin, Philipp Rümmer, andZhilin Wu. 2019. Decision procedures for path feasibility of stringmanipulating programs with complex operations. Proc. ACM Program.
Lang. 3, POPL (2019), 49:1–49:30. https://doi.org/10.1145/3290362[14] Lucas C. Cordeiro, Pascal Kesseli, Daniel Kroening, Peter Schrammel,and Marek Trtík. 2018. JBMC: A Bounded Model Checking Tool
for Verifying Java Bytecode. In Computer Aided Verification - 30th
International Conference, CAV 2018, Held as Part of the Federated Logic
Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, PartI (Lecture Notes in Computer Science, Vol. 10981), Hana Chockler andGeorg Weissenbacher (Eds.). Springer, 183–190. https://doi.org/10.
1007/978-3-319-96145-3_10[15] Loris D’Antoni and Margus Veanes. 2017. The Power of Symbolic
Automata and Transducers. In Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28,
2017, Proceedings, Part I (Lecture Notes in Computer Science, Vol. 10426),
Rupak Majumdar and Viktor Kuncak (Eds.). Springer, 47–67. https://doi.org/10.1007/978-3-319-63387-9_3[16] Loris D’Antoni and Margus Veanes. 2021. Automata modulo theories.
Commun. ACM 64, 5 (2021), 86–95. https://doi.org/10.1145/3419404[17] Leonardo Mendonça de Moura and Nikolaj Bjørner. 2008. Z3: An
Efficient SMT Solver. In Tools and Algorithms for the Construction andAnalysis of Systems, 14th International Conference, TACAS 2008, Heldas Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings (Lecture Notes in Computer Science, Vol. 4963), C. R. Ramakrishnan
and Jakob Rehof (Eds.). Springer, 337–340. https://doi.org/10.1007/9783-540-78800-3_24[18] 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.
[19] Burak Ekici, Guy Katz, Chantal Keller, Alain Mebsout, Andrew J.
Reynolds, and Cesare Tinelli. 2016. Extending SMTCoq, a Certified
Checker for SMT (Extended Abstract). In Proceedings First International

Acknowledgments
The authors would like to thank anonymous reviewers fortheir valuable comments. This research was supported in partby the ERC Starting Grant 759969 (AV-SMP), Max-Planck
Fellowship, Amazon Research Award, the Swedish ResearchCouncil (VR) under grant 2018-04727, and by the Swedish
Foundation for Strategic Research (SSF) under the project
WebSec (Ref. RIT17-0011).

References[1] 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 Computer Aided Verification - 26th
International Conference, CAV 2014, Held as Part of the Vienna Summerof Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings (Lecture
Notes in Computer Science, Vol. 8559), Armin Biere and Roderick Bloem(Eds.). Springer, 150–166. https://doi.org/10.1007/978-3-319-088679_10[2] Roberto Amadini, Mak Andrlon, Graeme Gange, Peter Schachte, Harald Søndergaard, and Peter J. Stuckey. 2019. Constraint Programmingfor Dynamic Symbolic Execution of JavaScript. In Integration of Constraint Programming, Artificial Intelligence, and Operations Research 16th International Conference, CPAIOR 2019, Thessaloniki, Greece, June
4-7, 2019, Proceedings (Lecture Notes in Computer Science, Vol. 11494),
Louis-Martin Rousseau and Kostas Stergiou (Eds.). Springer, 1–19.
https://doi.org/10.1007/978-3-030-19212-9_1[3] John Backes, Pauline Bolignano, Byron Cook, Catherine Dodge, Andrew Gacek, Kasper Søe Luckow, Neha Rungta, Oksana Tkachuk, andCarsten Varming. 2018. Semantic-based Automated Reasoning for
AWS Access Policies using SMT. In 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018, Nikolaj Bjørner and Arie Gurfinkel (Eds.). IEEE, 1–9.
https://doi.org/10.23919/FMCAD.2018.8602994[4] Murphy Berzish, Vijay Ganesh, and Yunhui Zheng. 2017. Z3str3: A
string solver with theory-aware heuristics. In 2017 Formal Methods
in Computer Aided Design, FMCAD 2017, Vienna, Austria, October 26, 2017, Daryl Stewart and Georg Weissenbacher (Eds.). IEEE, 55–59.
https://doi.org/10.23919/FMCAD.2017.8102241[5] Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel D.
Day, Dirk Nowotka, and Vijay Ganesh. 2021. An SMT Solver for
Regular Expressions and Linear Arithmetic over String Length. In
Computer Aided Verification - 33rd International Conference, CAV 2021,
Virtual Event, July 20-23, 2021, Proceedings, Part II (Lecture Notes in
Computer Science, Vol. 12760), Alexandra Silva and K. Rustan M. Leino(Eds.). Springer, 289–312. https://doi.org/10.1007/978-3-030-816889_14[6] Dmitry Blotsky, Federico Mora, Murphy Berzish, Yunhui Zheng, Ifaz
Kabir, and Vijay Ganesh. 2018. StringFuzz: A Fuzzer for String Solvers.
In Computer Aided Verification - 30th International Conference, CAV

CertiStr: A Certified String Solver
Workshop on Hammers for Type Theories, HaTT@IJCAR 2016, Coimbra,
Portugal, July 1, 2016 (EPTCS, Vol. 210), Jasmin Christian Blanchette andCezary Kaliszyk (Eds.). 21–29. https://doi.org/10.4204/EPTCS.210.5[20] Claudio Gutiérrez. 1998. Solving Equations in Strings: On Makanin’s
Algorithm. In LATIN ’98: Theoretical Informatics, Third Latin American
Symposium, Campinas, Brazil, April, 20-24, 1998, Proceedings (Lecture
Notes in Computer Science, Vol. 1380), Claudio L. Lucchesi and Arnaldo V.
Moura (Eds.). Springer, 358–373. https://doi.org/10.1007/BFb0054336[21] Matthew Hague, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu.
2020. Monadic Decomposition in Integer Linear Arithmetic. In Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris,
France, July 1-4, 2020, Proceedings, Part I (Lecture Notes in Computer
Science, Vol. 12166), Nicolas Peltier and Viorica Sofronie-Stokkermans(Eds.). Springer, 122–140. https://doi.org/10.1007/978-3-030-51074-9_8[22] Lukás Holík, Petr Janku, Anthony W. Lin, Philipp Rümmer, and Tomás
Vojnar. 2018. String constraints with concatenation and transducers
solved efficiently. Proc. ACM Program. Lang. 2, POPL (2018), 4:1–4:32.
https://doi.org/10.1145/3158092[23] Artur Jez. 2016. Recompression: A Simple and Powerful Techniquefor Word Equations. J. ACM 63, 1 (2016), 4:1–4:51. https://doi.org/10.
1145/2743014[24] Nils Klarlund, Anders Møller, and Michael I. Schwartzbach. 2002.
MONA Implementation Secrets. Int. J. Found. Comput. Sci. 13, 4 (2002),
571–586. https://doi.org/10.1142/S012905410200128X[25] Peter Lammich. 2013. Automatic Data Refinement. In Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July
22-26, 2013. Proceedings (Lecture Notes in Computer Science, Vol. 7998),
Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie (Eds.).
Springer, 84–99. https://doi.org/10.1007/978-3-642-39634-2_9[26] Peter Lammich. 2014. The CAVA Automata Isabelle Library. Arch.
Formal Proofs. https://www.isa-afp.org/entries/CAVA_Automata.
html.
[27] Peter Lammich and Andreas Lochbihler. 2010. The Isabelle Collections
Framework. In Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings (Lecture
Notes in Computer Science, Vol. 6172), Matt Kaufmann and Lawrence C.
Paulson (Eds.). Springer, 339–354. https://doi.org/10.1007/978-3-64214052-5_24[28] Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett, andMorgan Deters. 2014. A DPLL(T) Theory Solver for a Theory ofStrings and Regular Expressions. In Computer Aided Verification - 26th
International Conference, CAV 2014, Held as Part of the Vienna Summerof Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings (Lecture
Notes in Computer Science, Vol. 8559), Armin Biere and Roderick Bloem(Eds.). Springer, 646–662. https://doi.org/10.1007/978-3-319-088679_43[29] Anthony Widjaja Lin and Pablo Barceló. 2016. String solving with word
equations and transducers: towards a logic for analysing mutation XSS.
In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposiumon Principles of Programming Languages, POPL 2016, St. Petersburg, FL,
USA, January 20 - 22, 2016, Rastislav Bodík and Rupak Majumdar (Eds.).
ACM, 123–136. https://doi.org/10.1145/2837614.2837641[30] Gennady S Makanin. 1977. The problem of solvability of equations ina free semigroup. Sbornik: Mathematics 32, 2 (1977), 129–198.
[31] Muhammad Numair Mansur, Maria Christakis, Valentin Wüstholz,
and Fuyuan Zhang. 2020. Detecting critical bugs in SMT solvers using
blackbox mutational fuzzing. In ESEC/FSE ’20: 28th ACM Joint European
Software Engineering Conference and Symposium on the Foundations ofSoftware Engineering, Virtual Event, USA, November 8-13, 2020, Prem
Devanbu, Myra B. Cohen, and Thomas Zimmermann (Eds.). ACM,
701–712. https://doi.org/10.1145/3368089.3409763[32] Yasuhiko Minamide. 2005. Static approximation of dynamicallygenerated Web pages. In Proceedings of the 14th international conference on World Wide Web, WWW 2005, Chiba, Japan, May 10-14,

CPP ’22, January 17–18, 2022, Philadelphia, PA, USA
2005, Allan Ellis and Tatsuya Hagino (Eds.). ACM, 432–441. https://doi.org/10.1145/1060745.1060809[33] Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel. 2002. Isabelle/HOL: a proof assistant for higher-order logic. Vol. 2283. Springer
Science & Business Media.
[34] Yannic Noller, Corina S. Pasareanu, Aymeric Fromherz, XuanBach Dinh Le, and Willem Visser. 2019. Symbolic Pathfinder for SVCOMP - (Competition Contribution). In Tools and Algorithms for theConstruction and Analysis of Systems - 25 Years of TACAS: TOOLympics,
Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019,
Proceedings, Part III (Lecture Notes in Computer Science, Vol. 11429), Dirk
Beyer, Marieke Huisman, Fabrice Kordon, and Bernhard Steffen (Eds.).
Springer, 239–243. https://doi.org/10.1007/978-3-030-17502-3_21[35] Prateek Saxena, Devdatta Akhawe, Steve Hanna, Feng Mao, Stephen
McCamant, and Dawn Song. 2010. A Symbolic Execution Framework
for JavaScript. In 31st IEEE Symposium on Security and Privacy, S&P
2010, 16-19 May 2010, Berleley/Oakland, California, USA. IEEE Computer Society, 513–528. https://doi.org/10.1109/SP.2010.38[36] Xiaomu Shi, Yu-Fu Fu, Jiaxiang Liu, Ming-Hsien Tsai, Bow-Yaw
Wang, and Bo-Yin Yang. 2021. CoqQFBV: A Scalable Certified SMT
Quantifier-Free Bit-Vector Solver. In Computer Aided Verification - 33rd
International Conference, CAV 2021, Virtual Event, July 20-23, 2021,
Proceedings, Part II (Lecture Notes in Computer Science, Vol. 12760),
Alexandra Silva and K. Rustan M. Leino (Eds.). Springer, 149–171.
https://doi.org/10.1007/978-3-030-81688-9_7[37] Caleb Stanford, Margus Veanes, and Nikolaj Bjørner. 2021. Symbolic
Boolean derivatives for efficiently solving extended regular expression
constraints. In PLDI ’21: 42nd ACM SIGPLAN International Conference
on Programming Language Design and Implementation, Virtual Event,Canada, June 20-25, 2021, Stephen N. Freund and Eran Yahav (Eds.).
ACM, 620–635. https://doi.org/10.1145/3453483.3454066[38] Minh-Thai Trinh, Duc-Hiep Chu, and Joxan Jaffar. 2014. S3: A Symbolic String Solver for Vulnerability Detection in Web Applications.
In Proceedings of the 2014 ACM SIGSAC Conference on Computer andCommunications Security, Scottsdale, AZ, USA, November 3-7, 2014,
Gail-Joon Ahn, Moti Yung, and Ninghui Li (Eds.). ACM, 1232–1243.
https://doi.org/10.1145/2660267.2660372[39] 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 (Lecture Notes in Computer Science, Vol. 9779), Swarat Chaudhuri and Azadeh Farzan (Eds.). Springer,
218–240. https://doi.org/10.1007/978-3-319-41528-4_12[40] Thomas Tuerk. 2012. A Formalisation of Finite Automata in Isabelle /HOL. https://www.thomas-tuerk.de/assets/talks/cava.pdf.
[41] Margus Veanes, Pieter Hooimeijer, Benjamin Livshits, David Molnar,
and Nikolaj Bjørner. 2012. Symbolic finite state transducers: algorithms and applications. In Proceedings of the 39th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL
2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012, John Field
and Michael Hicks (Eds.). ACM, 137–150. https://doi.org/10.1145/
2103656.2103674[42] Hung-En Wang, Tzung-Lin Tsai, Chun-Han Lin, Fang Yu, and JieHong 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), Swarat Chaudhuri and Azadeh Farzan (Eds.). Springer, 241–260. https://doi.org/10.1007/978-3-319-41528-4_13[43] Fang Yu, Muath Alkhalaf, Tevfik Bultan, and Oscar H. Ibarra. 2014.
Automata-based symbolic string analysis for vulnerability detection.
Formal Methods Syst. Des. 44, 1 (2014), 44–70. https://doi.org/10.1007/
s10703-013-0189-1