Towards Constraint Logic Programming over Strings for Test Data Generation

Dierk Ehmke; Jannik Dunkelau; Joshua Schmidt; Patrick Skowronek; Sebastian Krings

REVIEW 3 major objections 5 minor 39 references

Towards Constraint Logic Programming over Strings for Test Data Generation

T0 review · 3 major / 5 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read A constraint logic programming solver over strings can generate valid test data from declarative specifications.

desk verdict Honest feasibility report; the prototype is plausible, but the case studies sidestep the hard concatenation case that would justify the general claim. read the letter →

arxiv 1908.10203 v1 pith:2EEYEXDW submitted 2019-08-27 cs.LO cs.SE

Sebastian Krings , Joshua Schmidt , Patrick Skowronek , Jannik Dunkelau , Dierk Ehmke This is my paper · ORCID

classification cs.LOcs.SE

keywords constraintlogicprogrammingstringconstraintstestdatagenerationfiniteautomataHandlingRulesregularexpressionssyntheticProlog

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper asks whether constraint logic programming can generate synthetic test data, with strings as the focus. It introduces ConString, a prototype CLP solver that represents string domains as finite automata and uses constraint handling rules to propagate information until the constraint store reaches a fixed point. The solver supports unbounded strings, regular expressions, concatenation, length constraints, and conversions between strings and integers, reals, and booleans. As evidence, it generates valid German IBANs and calendar-date expressions, and on the IBAN benchmark it runs in times comparable to an existing dedicated string solver. If the approach scales, testers could describe desired data declaratively instead of hand-crafting or copying production data.

What carries the argument

The load-bearing object is the finite automaton domain: each string variable's possible values are represented as a non-deterministic finite automaton with epsilon-transitions, encoded as a term with states, transition ranges, and initial and final states. This representation makes constraint propagation possible, because membership constraints intersect automata, concatenation combines them by linking final states to initial states of the next automaton, and labeling enumerates accepting words through backtracking search. Constraint Handling Rules drive the propagation to a fixed point, and conversion constraints connect the automaton domains to CLP(FD), CLP(R), and CLP(B), letting arithmetic constraints narrow string domains and vice versa.

What would settle it

Run ConString on a constraint system with an open interval concatenation, for example one where a generated string must combine an unbounded regular part with a fixed remainder and the solver must enumerate valid values; if the solver fails to terminate or cannot return a sample within a bounded time, the central feasibility claim is refuted.

Watch

Extended reading notes

Core claim

ConString shows that a constraint logic programming system over strings can handle realistic test-data generation tasks. Its central claim is that representing string domains as finite automata and propagating constraints through CHR is a workable design: for German IBANs, the solver computes checksums from mixed arithmetic and string constraints and generates up to 250,000 samples with wall-clock times close to those of the purpose-built CLPQS solver; for calendar dates, it builds up date expressions from regular expressions for weekdays, months, days, and years, although here it is markedly slower. The authors conclude that the approach is feasible and promising, while explicitly noting that only two small case studies were shown and that complex examples such as open interval concatenation remain untested.

Load-bearing premise

The general feasibility claim rests on two small case studies; if a more complex benchmark such as open interval concatenation exposes scaling or expressiveness failures, the claim that CLP over strings is feasible for test data generation would not survive.

Editorial extensions

If this is right

Test data can be specified declaratively as string constraints, so a tester need not implement a bespoke generator for each new format.
Because labeling enumerates the language of an automaton, one constraint system can produce many distinct valid values, giving the diversity that hand-crafted test data often lacks.
Mixing string domains with integer, real, and boolean constraints through conversion constraints makes it possible to generate data whose validity depends on arithmetic checks, as with IBAN checksums.
On the IBAN case study the prototype is competitive with a dedicated solver, which suggests that CLP over strings can be practical at least for moderate-sized generation tasks.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

If the automaton representation is the main bottleneck in date-like examples, switching to epsilon-free deterministic automata, as the paper itself anticipates, should reduce the performance gap on union-heavy constraints.
The all-solutions enumeration capability suggests a natural extension to fuzzing-style test generation: randomize the labeling order to sample diverse values from the same constraint system.
A direct test of the paper's proposed solver portfolio would be to run the same IBAN and date constraints on an SMT solver configured to return many models; the paper reports that the SMT solvers it tried could not produce multiple solutions.
The untested open interval concatenation case is the closest thing to a benchmark that would stress unboundedness; a positive result there would substantially strengthen the feasibility claim.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

First, the bottom line: this is a small, honest feasibility report about a CHR-based string constraint solver in SWI-Prolog. The prototype itself is the new artifact; the ingredients are all from the literature. The two case studies work, the write-up is clear, and the authors admit the big limitation in Section 6.3: no complex case like open interval concatenation. That admission is accurate, and it matters more than the paper lets on.

The good parts: the constraint models in Listings 5 and 6 are clean, the IBAN example meaningfully mixes CLP(FD) with string constraints, and the benchmarking against CLPQS and a quick SMT comparison is a reasonable check. The paper is refreshingly direct about what is missing.

Now the soft spots. The 'feasible and promising' conclusion is supported by exactly two benchmarks, and both are constructed so they never require general backward propagation through concatenation. Listing 2 only has forward rules from S1 and S2 domains to S3; the only reverse direction handles a constant string result by enumerating all splits with SWI-Prolog's string_concat. If the result has a non-trivial regular-language domain and you need to infer the operands, there is no propagation rule. The IBAN case labels the integer BBAN first and then assembles the string with constant concatenation; the date case labels a precomputed automaton. Neither exercises the operation that makes string constraint solving hard, so the general claim outruns the evidence. The paper says exactly this in Section 6.3, so it's not a hidden flaw, but the conclusion should have been hedged accordingly.

Minor issues: no released code, no validation that generated strings are correct beyond the solver's own construction, and benchmark tables report medians of five runs without any variance. For a prototype paper these are acceptable, but they are part of why the evidence is thin.

Who should read this: anyone working on CLP over strings or tool-oriented test data generation. It's a useful data point, not a milestone. If I were the editor, I'd send it to peer review for a workshop or short-paper venue, asking the authors to release the artifact and add one case that actually forces reverse propagation through concatenation. The prototype is plausible; the general claim is not yet established.

Referee Report

3 major / 5 minor

Summary. The paper presents ConString, a prototypical constraint logic programming system over strings built with Constraint Handling Rules (CHR) on top of SWI-Prolog. String domains are represented as nondeterministic finite automata with epsilon transitions, and the system integrates with CLP(FD), CLP(R), and CLP(B) for mixed-domain constraints. The authors demonstrate the approach on two test-data generation benchmarks: German IBAN numbers and calendar date expressions. They compare wall-clock performance with their earlier CLPQS solver and with Z3-str3 and CVC4 on encodings of the same examples, and conclude that the approach is 'feasible and promising.'

Significance. If the central claim is accepted, ConString provides a useful declarative alternative to existing string solvers for test-data generation, with composable automaton domains and native integration with other constraint solvers. The paper's concrete strengths are its transparent CHR rule listings, the automaton-based domain representation, and the IBAN constraint model, which encodes the checksum arithmetic in a readable way. However, the evidence for feasibility is thin: no code is released, the benchmarks are small, the comparison reports only medians without variance, and the most challenging string operation for this domain representation, backward propagation through concatenation with unbounded domains, is not exercised by either case study. The manuscript is honestly scoped as a prototype description, but the strength of the conclusion is not matched by the supporting evidence.

major comments (3)

[§6.3 and §4.3, Listings 2 and 5-6] The paper's own limitation statement in §6.3 concedes that no complex case study such as an open interval concatenation was shown. This is not just a missing benchmark: it is the operation for which ConString lacks a general backward propagation rule. Listing 2 derives a result domain only from the domains of the two arguments, and the only reverse direction described in §4.3 enumerates splits when the result is a constant string. If S3 has a non-constant regular-language domain and S1 and S2 must be inferred, the solver has no propagation rule and must fall back to generate-and-test at labeling time. The IBAN example avoids this by labeling the CLP(FD) integer BBAN first and then assembling the string through constant concatenation; the date example labels a single precomputed automaton for the whole expression. Because concatenation with unbounded domains is a known source of hardness in string constraint solving, these examples do not support the general conclusion that the approach is 'feasible and promising' for the SQL-style string operations listed in §2.2.
[§5.1, §5.2, Tables 2 and 3] The benchmark evaluation provides no independent validation that the generated strings are correct. For test-data generation, validity of the produced data is a central requirement, yet the paper does not report checking, outside the constraint system, that generated IBANs satisfy the checksum or that generated date expressions are accepted by an independent parser. Additionally, the performance tables report only the median of five wall-clock runs, with no min/max, standard deviation, or statistical comparison, which makes the claimed performance differences difficult to assess. The non-linear growth attributed to SWI-Prolog's CLP(FD) in §5.1 is also not substantiated with profiling data. These omissions weaken the central feasibility claim.
[§2.2, §4.3, Table 1] The paper motivates the solver with a list of SQL string operations in §2.2 (CONCAT, LENGTH, REGEXP, SUBSTRING, TO_NUMBER) and gives a feature matrix in Table 1, but it never provides a direct mapping from those requirements to the operations actually implemented in ConString. The implementation described in §4.3 supports membership, concatenation, iteration, prefix/suffix/infix, length, and conversions, but the handling of REGEXP is not demonstrated, and the rules in Listings 2-4 only show forward propagation for concatenation and constant reverse cases. For a reader evaluating feasibility, it is unclear which of the requirements in §2.2 are fully supported by the prototype and which are only partially supported or not supported at all.

minor comments (5)

[Abstract] The abstract contains a typo: 'calender dates' should be 'calendar dates', and the title in the arXiv header begins with 'T owards' instead of 'Towards'.
[Listing 5] Listing 5 contains garbled identifiers due to line-breaking: 'str_concate na ti o n' should be 'str_concatenation', and the variable 'IBANPrefix' is used but the code as printed is hard to read. Please reformat the listing.
[§5.2] In the text describing Listing 6, 'MondDay' is a typo for 'MonthDay', and the shorthand notation using 'match' and '\/' is not explained before its first use.
[Tables 2 and 3] The column heading 'Amount' is unclear; it should be stated explicitly that the values are the number of generated strings. In Table 3, all CLPQS times are reported as 0.000 seconds, which is likely a rounding artifact; please report timing precision or use a smaller unit.
[§3.5 and Table 1] The text in §3.5 says that 'no single approach is able to satisfactorily handle the requirements', but Table 1 marks CLPQS as fully supporting all listed requirements. This apparent inconsistency should be clarified.

Circularity Check

0 steps flagged · score 2.0 of 10

No circular derivation; the feasibility claim rests on prototype benchmarks, with only a minor non-load-bearing self-citation to the authors' earlier CLPQS solver.

full rationale

The paper's central claim is that its CLP-over-strings prototype ConString is feasible and promising for test data generation. That claim is supported by two implemented case studies and wall-clock benchmarks, not by deriving the prototype's semantics from the benchmarks. The CHR propagation rules in Section 4.3 (e.g., str_concat/3 in Listing 2) are defined directly over finite-automaton domains, and the benchmark results are external measurements of those rules; no parameter in the solver is fitted to the IBAN or date outputs, and no equation used in the evaluation is defined in terms of the evaluation's success. The only notable self-reference is that the primary baseline, CLPQS, is an earlier solver from the same group (Friske and Ehmke, reference [10], with co-author Ehmke), and reference [23] is the authors' own prior work on combining solvers. These citations are used for context and baseline comparison, not as the justification for ConString's correctness or for the propagation rules. The IBAN constraint model is taken from [10] and the date grammar from external reference [19], but importing a benchmark model is not circular. The admitted limitation in Section 6.3, that no complex case study such as open interval concatenation was shown, is a threat to the generality of the feasibility conclusion, but it is an external-validity gap, not a circular derivation. Thus there is no significant circularity; the minor self-citation warrants a low nonzero score rather than a zero.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

No free parameters are fitted to data: ConString is a deterministic prototype with no tuned constants. The central claim rests on standard automata closure facts, an unproven correctness assumption for the CHR propagation, and the representativeness of the two case studies. No new physical, mathematical, or software entities are postulated beyond the prototype itself.

assumptions (3)

standard math Regular languages are closed under union, intersection, concatenation, and iteration.
Section 4.2 uses finite automata as string domains and relies on these closure properties to implement operations; this is a standard textbook fact.
domain assumption The CHR rules and automata operations implement correct constraint propagation for the supported string constraints.
Section 4.3 states 'we ensure arc- and path-consistency of our constraints' without a correctness proof; the benchmark results presume the solver returns only valid strings.
domain assumption Two small case studies are representative of realistic test data generation tasks.
Section 6.3 admits the paper 'showed two small and realistic use cases' and no complex case; the feasibility conclusion depends on this representativeness.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Towards Constraint Logic Programming over Strings for Test Data Generation." pith.science (2026). https://pith.science/paper/2EEYEXDW

@misc{pith2026190810203,
  author       = {Pith},
  title        = {Pith review of: Towards Constraint Logic Programming over Strings for Test Data Generation},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/2EEYEXDW}},
  note         = {Machine review of arXiv:1908.10203}
}

read the original abstract

In order to properly test software, test data of a certain quality is needed. However, useful test data is often unavailable: Existing or hand-crafted data might not be diverse enough to enable desired test cases. Furthermore, using production data might be prohibited due to security or privacy concerns or other regulations. At the same time, existing tools for test data generation are often limited. In this paper, we evaluate to what extent constraint logic programming can be used to generate test data, focussing on strings in particular. To do so, we introduce a prototypical CLP solver over string constraints. As case studies, we use it to generate IBAN numbers and calender dates.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

39 extracted references · 39 canonical work pages

[1]

P. A. Abdulla, M. F. Atig, Y. Chen, B. P. Diep, L. Holík, A. Re zine, and P. Rüm- mer. Trau: SMT solver for string constraints. In 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - Novem ber 2, 2018 , pages 1–5, 2018

work page 2018
[2]

P. A. Abdulla, M. F. Atig, Y.-F. Chen, B. P. Diep, L. Holík, A . Rezine, and P. Rümmer. Flatten and Conquer: A Framework for Eﬃcient Anal ysis of String Constraints. In Proceedings of the 38th ACM SIGPLAN Conference on Program- ming Language Design and Implementation , PLDI 2017, pages 602–617. ACM, 2017

work page 2017
[3]

MiniZinc with Strings

R. Amadini, P. Flener, J. Pearson, J. D. Scott, P. J. Stucke y, and G. Tack. MiniZinc with Strings. CoRR, abs/1608.03650, 2016

work page Pith review arXiv 2016
[4]

Amadini, G

R. Amadini, G. Gange, P. Stuckey, and G. Tack. A Novel Appro ach to String Constraint Solving. pages 3–20, 08 2017

work page 2017
[5]

Barrett, C

C. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovano vi’c, T. King, A. Reynolds, and C. Tinelli. CVC4. In G. Gopalakrishnan and S . Qadeer, editors, Proceedings of the 23rd International Conference on Comput er Aided Veriﬁcation (CA V ’11), volume 6806 of LNCS, pages 171–177. Springer, July 2011

work page 2011
[6]

Berzish, V

M. Berzish, V. Ganesh, and Y. Zheng. Z3str3: A string solve r with theory-aware heuristics. In FMCAD, pages 55–59. IEEE, 2017

work page 2017
[7]

T. Chen, Y. Chen, M. Hague, A. W. Lin, and Z. Wu. What Is Decid able about String Constraints with the ReplaceAll Function. CoRR, abs/1711.03363, 2017

work page Pith review arXiv 2017
[8]

de Moura and N

L. de Moura and N. Bjørner. Z3: An Eﬃcient SMT Solver. In Proceedings TACAS, volume 4963 of LNCS, pages 337–340. Springer, 2008

work page 2008

Show all 39 references

[9]

ElGamal, A

N. ElGamal, A. ElBastawissy, and G. Galal-Edeen. Data War ehouse Testing. In Proceedings EDBT/ICDT, EDBT ’13, pages 1–8. ACM, 2013

2013
[10]

Friske and D

M. Friske and D. Ehmke. Modellbasierte Testdatenspeziﬁ kation und -generierung mittels Äquivalenzklassen und SQL. In Proceedings TA V, 02 2019

2019
[11]

Frühwirth

T. Frühwirth. Theory and practice of constraint handlin g rules. The Journal of Logic Programming, 37(1–3):95–138, 1998

1998
[12]

Fu and C.-C

X. Fu and C.-C. Li. A String Constraint Solver for Detecti ng Web Application Vulnerability. pages 535–542, 01 2010

2010
[13]

Ganesh and D

V. Ganesh and D. L. Dill. A Decision Procedure for Bit-vec tors and Arrays. In Proceedings CA V, CA V’07, pages 519–531. Springer, 2007

2007
[14]

Golden and W

K. Golden and W. Pang. Constraint Reasoning over Strings . In F. Rossi, editor, Proceedings CP, pages 377–391. Springer, 2003

2003
[15]

Haftmann, D

F. Haftmann, D. Kossmann, and E. Lo. A framework for eﬃcie nt regression tests on database applications. The VLDB Journal , 16(1):145–164, Jan 2007

2007
[16]

Houkjær, K

K. Houkjær, K. Torp, and R. Wind. Simple and Realistic Dat a Generation. In VLDB, 2006

2006
[17]

Standard, International Organiza tion for Standardiza- tion, Geneva, CH, 6 2017

Information technology – Security techniques – Informa tion security management systems – Requirements. Standard, International Organiza tion for Standardiza- tion, Geneva, CH, 6 2017

2017
[18]

D. R. Jeske, P. J. Lin, C. Rendon, R. Xiao, and B. Samadi. Sy nthetic Data Generation Capabilties for Testing Data Mining Tools. In Proceedings MILCOM, pages 1–6, Oct 2006

2006
[19]

Karttunen, J.-P

L. Karttunen, J.-P. Chanod, G. Grefenstette, and A. Schi lle. Regular expressions for language engineering. Natural Language Engineering , 2(4):305–328, 1996

1996
[20]

M. S. A. Khan and A. ElMadi. Data Warehouse Testing an Expl oratory Study. Master’s thesis, School of Computing, Blekinge Institute o f Technology, Karl- skrona, Sweden, 2011

2011
[21]

Kieżun, V

A. Kieżun, V. Ganesh, P. J. Guo, P. Hooimeijer, and M. D. Er nst. HAMPI: A solver for string constraints. In Proceedings ISSTA 2009, July 21–23, 2009

2009
[22]

E. K. Klaus Franz, Tanja Tremmel. Basiswissen Testdatenmanagement: Aus- und Weiterbildung zum Test Data Specialist – Certiﬁed Tester Fo undation Level nach GTB. dpunkt, 2018

2018
[23]

Krings and M

S. Krings and M. Leuschel. SMT Solvers for Validation of B and Event-B models. In Proceedings iFM, volume 9681 of LNCS. Springer, 2016

2016
[24]

Liang, A

T. Liang, A. Reynolds, C. Tinelli, C. Barrett, and M. Dete rs. A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions. page s 646–662, 07 2014

2014
[25]

Liang, A

T. Liang, A. Reynolds, N. Tsiskaridze, C. Tinelli, C. Bar rett, and M. Deters. An Eﬃcient SMT Solver for String Constraints. Form. Methods Syst. Des. , 48(3):206– 234, June 2016

2016
[26]

A. Møller. dk.brics.automaton – ﬁnite-state automata a nd regular expressions for Java, 2017. http://www.brics.dk/automaton/

2017
[27]

Pretschner

A. Pretschner. Zum modellbasierten funktionalen Test r eaktiver Systeme. 2003. http://mediatum.ub.tum.de/doc/601738/000006bb.pdf

2003
[28]

Schulte, G

C. Schulte, G. Tack, and M. Z. Lagerkvist. Modeling and pr ogramming with gecode. Schulte, Christian and Tack, Guido and Lagerkvist, Mikael , 2015, 2010

2015
[29]

Singh and K

J. Singh and K. Singh. Statistically Analyzing the Impac t of Automated ETL Testing on the Data Quality of a Data Warehouse. IJCEE, 1(4):488–495, 2009

2009
[30]

Spillner and T

A. Spillner and T. Linz. Basiswissen Softwaretest: Aus- und Weiterbildung zum Certiﬁed Tester – Foundation Level nach ISTQB-Standard . dpunkt, 3. edition, 2005

2005
[31]

Tillmann and J

N. Tillmann and J. De Halleux. Pex: White Box Test Generat ion for .NET. In Proceedings TAP, TAP’08, pages 134–153. Springer, 2008

2008
[32]

Tinelli, C

C. Tinelli, C. Barret, and P. Fontaine. Unicode Strings ( Draft 2.0), 2019. http:// smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml

2019
[33]

Trinh, D.-H

M.-T. Trinh, D.-H. Chu, and J. Jaﬀar. S3: A Symbolic Strin g Solver for Vulnerabil- ity Detection in Web Applications. In Proceedings CCS, CCS ’14, pages 1232–1243. ACM, 2014

2014
[34]

M. Triska. The ﬁnite domain constraint solver of SWI-Pro log. In Proceedings FLOPS, volume 7294 of LNCS, pages 307–316, 2012

2012
[35]

M. Triska. The Boolean Constraint Solver of SWI-Prolog: System Description. In Proceedings FLOPS, volume 9613 of LNCS, pages 45–61, 2016

2016
[36]

M. Triska. Boolean constraints in SWI-Prolog: A compreh ensive system descrip- tion. Science of Computer Programming , 164:98–115, 2018

2018
[37]

Wielemaker, T

J. Wielemaker, T. Schrijvers, M. Triska, and T. Lager. SW I-Prolog. CoRR, abs/1011.5332, 2010

2010 arXiv
[38]

Zheng, V

Y. Zheng, V. Ganesh, S. Subramanian, O. Tripp, M. Berzish , J. Dolby, and X. Zhang. Z3str2: an eﬃcient solver for strings, regular exp ressions, and length constraints. Formal Methods in System Design , 50(2-3):249–288, 2017

2017
[39]

Zheng, X

Y. Zheng, X. Zhang, and V. Ganesh. Z3-str: A Z3-based Stri ng Solver for Web Application Analysis. In Proceedings ESEC/FSE, ESEC/FSE 2013, pages 114–124. ACM, 2013

2013

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.

[1] [1]

P. A. Abdulla, M. F. Atig, Y. Chen, B. P. Diep, L. Holík, A. Re zine, and P. Rüm- mer. Trau: SMT solver for string constraints. In 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - Novem ber 2, 2018 , pages 1–5, 2018

work page 2018

[2] [2]

P. A. Abdulla, M. F. Atig, Y.-F. Chen, B. P. Diep, L. Holík, A . Rezine, and P. Rümmer. Flatten and Conquer: A Framework for Eﬃcient Anal ysis of String Constraints. In Proceedings of the 38th ACM SIGPLAN Conference on Program- ming Language Design and Implementation , PLDI 2017, pages 602–617. ACM, 2017

work page 2017

[3] [3]

MiniZinc with Strings

R. Amadini, P. Flener, J. Pearson, J. D. Scott, P. J. Stucke y, and G. Tack. MiniZinc with Strings. CoRR, abs/1608.03650, 2016

work page Pith review arXiv 2016

[4] [4]

Amadini, G

R. Amadini, G. Gange, P. Stuckey, and G. Tack. A Novel Appro ach to String Constraint Solving. pages 3–20, 08 2017

work page 2017

[5] [5]

Barrett, C

C. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovano vi’c, T. King, A. Reynolds, and C. Tinelli. CVC4. In G. Gopalakrishnan and S . Qadeer, editors, Proceedings of the 23rd International Conference on Comput er Aided Veriﬁcation (CA V ’11), volume 6806 of LNCS, pages 171–177. Springer, July 2011

work page 2011

[6] [6]

Berzish, V

M. Berzish, V. Ganesh, and Y. Zheng. Z3str3: A string solve r with theory-aware heuristics. In FMCAD, pages 55–59. IEEE, 2017

work page 2017

[7] [7]

T. Chen, Y. Chen, M. Hague, A. W. Lin, and Z. Wu. What Is Decid able about String Constraints with the ReplaceAll Function. CoRR, abs/1711.03363, 2017

work page Pith review arXiv 2017

[8] [8]

de Moura and N

L. de Moura and N. Bjørner. Z3: An Eﬃcient SMT Solver. In Proceedings TACAS, volume 4963 of LNCS, pages 337–340. Springer, 2008

work page 2008