检索结果-内蒙古大学图书馆

An efficient string solver for string constraints with regex-counting and string-length

JOURNAL OF SYSTEMS ARCHITECTURE 2025年 160卷

作者： Hu, Denghang Wu, Zhilin Univ Chinese Acad Sci Chinese Acad Sci Inst Software Key Lab Syst Software Beijing Peoples R China Univ Chinese Acad Sci Chinese Acad Sci Inst Software State Key Lab Comp Sci Beijing Peoples R China

Regular expressions (regex for short) and string-length function are widely used in string-manipulating programs. Counting is a frequently used feature in regexes that counts the number of matchings of sub- patterns. The state-of-the-art string solvers are incapable of solving string constraints with regex-counting and string-length efficiently, especially when the counting and length bounds are large. In this work, we propose an automata-theoretic approach for solving such class of string constraints. The main idea is to symbolically model the counting operators by registers in automata instead of unfolding them explicitly, thus alleviating the state explosion problem. Moreover, the string-length function is modeled by a register as well. As a result, the satisfiability of string constraints with regex-counting and string-length is reduced to the satisfiability of linear integer arithmetic, which the off-the-shelf SMT solvers can then solve. To improve the performance further, we also propose various optimization techniques. We implement the algorithms and validate our approach on 49,843 benchmark instances. The experimental results show that our approach can solve more instances than the state-of-the-art solvers, at a comparable or faster speed, especially when the counting and length bounds are large or when the counting operators are nested with some other counting operators or complement operators.

关键词： string constraints string solver Regular expression string length Counting operator

来源：评论

学校读者我要写书评

暂无评论

Towards more efficient methods for solving regular-expression heavy string constraints

引用

THEORETICAL COMPUTER SCIENCE 2023年第1期943卷 50-72页

作者： Berzish, Murphy Day, Joel D. Ganesh, Vijay Kulczynski, Mitja Manea, Florin Mora, Federico Nowotka, Dirk Univ Waterloo Waterloo ON Canada Loughborough Univ Loughborough England Univ Kiel Kiel Germany Univ Gottingen Gottingen Germany Univ Gottingen Campus Inst Data Sci Gottingen Germany Univ Calif Berkeley Berkeley CA USA

Widespread use of string solvers in the formal analysis of string-heavy programs has led to a growing demand for more efficient and reliable techniques which can be applied in this context. Designing practical algorithms for the (generally undecidable) satisfiability problem for systems of string constraints requires a deep understanding of the structure of constraints present in the targeted cases. In this paper, we first investigate relevant benchmarks containing regular expression membership predicates, extract a series of first order logic theories, and prove the decidability, respectively undecidability, of their satisfiability problem. Further, building on the theoretical results, we present a novel length-aware solving algorithm for the quantifier-free first-order theory over regular expression membership predicates and linear arithmetic over string length. We implement and evaluate this algorithm and related heuristics in the Z3 theorem prover. Besides the theoretical aspects leading to this algorithm, a crucial insight that underpins it is that real -world regex and string formulas contain a wealth of information about upper and lower bounds on lengths of strings, and such information can be used very effectively to simplify operations on automata representing regular expressions. Additionally, we present several novel general heuristics, such as the prefix/suffix method, that can be used to make a variety of regex solving algorithms more efficient in practice. We showcase the power of our algorithm and heuristics via an extensive empirical evaluation over a large and diverse benchmark of 57256 regex-heavy instances, almost 75% of which are derived from industrial applications or contributed by other solver developers. Our solver outperforms five other state-of-the-art string solvers over this benchmark. (c) 2022 Elsevier B.V. All rights reserved.

关键词： SMT solving string solving string constraints Regular expressions Linear length constraints Heuristics

来源：评论

学校读者我要写书评

暂无评论

On the Expressive Power of string constraints

引用

PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL 2023年第POPL期7卷 278-308页

作者： Day, Joel D. Ganesh, Vijay Grewal, Nathan Manea, Florin Loughborough Univ Loughborough Leics England Univ Waterloo Waterloo ON Canada Univ Gottingen Gottingen Germany

We investigate properties of strings which are expressible by canonical types of string constraints. Specifically we consider a landscape of 20 logical theories, whose syntax is built around combinations of four common elements of string constraints: language membership (e.g. for regular languages), concatenation, equality between string terms, and equality between string-lengths. For a variable x and formula f from a given theory, we consider the set of values for which x may be substituted as part of a satisfying assignment, or in other words, the property f expresses through x. Since we consider string-based logics, this set is a formal language. We firstly consider the relative expressive power of different combinations of string constraints by comparing the classes of languages expressible in the corresponding theories, and are able to establish a mostly complete picture in this regard. Secondly, we consider the question of deciding whether the language or property expressed by a variable/formula in one theory can be expressed in another theory. We establish several negative results which are relevant to preprocessing and normalisation of string constraints in practice. Some of our results have strong connections to important open problems regarding word equations and the theory of string solving.

关键词： string constraints string solving Word equations

来源：评论

学校读者我要写书评

暂无评论

Solving string constraints with Lengths by Stabilization

引用

PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL 2023年第OOPSLA期7卷 2112–2141页

作者： Chen, Yu-Fang Chocholaty, David Havlena, Vojtech Holik, Lukas Lengal, Ondrej Sic, Juraj Acad Sinica Inst Informat Sci Taipei Taiwan Brno Univ Technol Fac Informat Technol Brno Czech Republic

We present a new algorithm for solving string constraints. The algorithm builds upon a recent method for solving word equations and regular constraints that interprets string variables as languages rather than strings and, consequently, mitigates the combinatorial explosion that plagues other approaches. We extend the approach to handle linear integer arithmetic length constraints by combination with a known principle of equation alignment and splitting, and by extension to other common types of string constraints, yielding a fully-fledged string solver. The ability of the framework to handle unrestricted disequalities even extends one of the largest decidable classes of string constraints, the chain-free fragment. We integrate our algorithm into a DPLL-based SMT solver. The performance of our implementation is competitive and even significantly better than state-of-the-art string solvers on several established benchmarks obtained from applications in verification of string programs.

关键词： string constraints stabilization word equations SMT solving length constraints regular languages

来源：评论

学校读者我要写书评

暂无评论

Satisfiability of Context-Free string constraints with Subword-Ordering and Transducers 41

Satisfiability of Context-Free String Constraints with Subwo...

引用

41st International Symposium on Theoretical Aspects of Computer Science (STACS)

作者： Aiswarya, C. Mal, Soumodev Saivasan, Prakash Chennai Math Inst Chennai Tamil Nadu India CNRS ReLaX IRL 2000 Chennai Tamil Nadu India HBNI Inst Math Sci Chennai Tamil Nadu India

ISBN: (纸本)9783959773119

We study the satisfiability of string constraints where context-free membership constraints may be imposed on variables. Additionally a variable may be constrained to be a subword of a word obtained by shuffling variables and their transductions. The satisfiability problem is known to be undecidable even without rational transductions. It is known to be NExptime-complete without transductions, if the subword relations between variables do not have a cyclic dependency between them. We show that the satisfiability problem stays decidable in this fragment even when rational transductions are added. It is 2NEXPTIME-complete with context-free membership, and NExptime-complete with only regular membership. For the lower bound we prove a technical lemma that is of independent interest: The length of the shortest word in the intersection of a pushdown automaton (of size O(n)) and n finite-state automata (each of size O(n)) can be double exponential in n.

关键词： satisfiability subword string constraints context-free transducers

来源：评论

学校读者我要写书评

暂无评论

Accurate string constraints Solution Counting with Weighted Automata 34

Accurate String Constraints Solution Counting with Weighted ...

引用

34th IEEE/ACM International Conference on Automated Software Engineering (ASE)

作者： Sherman, Elena Harris, Andrew Boise State Univ Comp Sci Dept Boise ID 83725 USA

ISBN: (纸本)9781728125084

As an important extension of symbolic execution (SE), probabilistic symbolic execution (PSE) computes execution probabilities of program paths. Using this information, PSE can prioritize path exploration strategies. To calculate the probability of a path PSE relies on solution counting approaches for the path constraint. The correctness of a solution counting approach depends on the methodology used to count solutions and whether a path constraint maintains a one-to-one relation with program input values. This work focuses on the latter aspect of the solution counting correctness for string constraints. In general, maintaining a one-to-one relation is not always possible, especially in the presence of non-linear constraints. To deal with this issue, researchers that work on PSE for numerical domains either analyze programs with linear constraints, or develop novel techniques to handle solution counting of non-linear constraints. For the string domain, however, previous work on PSE mainly focuses on efficient and accurate solution counting for automata-based string models and has not investigated whether a one-to-one relationship between the strings encoded by automata and input string values is preserved. In this work we demonstrate that traditional automata-based string models fail to maintain one-to-one relations and propose to use the weighted automata model, which preserves the one-to-one relation between the path constraint it encodes and the input string values. We use this model to implement a string constraint solver and show its correctness on a set of non-trivial synthetic benchmarks. We also present an empirical evaluation of traditional and proposed automata solvers on real-world string constraints. The evaluations show that while being less efficient than traditional automata models, the weighted automata model maintains correct solution counts.

关键词： probabilistic symbolic execution string constraints quantitative program analysis

来源：评论

学校读者我要写书评

暂无评论

Chain-Free string constraints 17th

Chain-Free String Constraints

引用

17th International Symposium on Automated Technology for Verification and Analysis (ATVA)

作者： Abdulla, Parosh Aziz Atig, Mohamed Faouzi Bui Phi Diep Holik, Lukas Janku, Petr Uppsala Univ Uppsala Sweden Brno Univ Technol Brno Czech Republic

ISBN: (纸本)9783030317843;9783030317836

We address the satisfiability problem for string constraints that combine relational constraints represented by transducers, word equations, and string length constraints. This problem is undecidable in general. Therefore, we propose a new decidable fragment of string constraints, called weakly chaining string constraints, for which we show that the satisfiability problem is decidable. This fragment pushes the borders of decidability of string constraints by generalising the existing straight-line as well as the acyclic fragment of the string logic. We have developed a prototype implementation of our new decision procedure, and integrated it into in an existing framework that uses CEGAR with under-approximation of string constraints based on flattening. Our experimental results show the competitiveness and accuracy of the new framework.

关键词： string constraints Satisfiability modulo theories Program verification

来源：评论

学校读者我要写书评

暂无评论

Accurate string constraints solution counting with weighted automata 19

Accurate string constraints solution counting with weighted ...

引用

Proceedings of the 34th IEEE/ACM International Conference on Automated Software Engineering

作者： Elena Sherman Andrew Harris Boise State University

ISBN: (纸本)9781728125084

As an important extension of symbolic execution (SE), probabilistic symbolic execution (PSE) computes execution probabilities of program paths. Using this information, PSE can prioritize path exploration strategies. To calculate the probability of a path PSE relies on solution counting approaches for the path constraint. The correctness of a solution counting approach depends on the methodology used to count solutions and whether a path constraint maintains a one-to-one relation with program input values. This work focuses on the latter aspect of the solution counting correctness for string *** general, maintaining a one-to-one relation is not always possible, especially in the presence of non-linear constraints. To deal with this issue, researchers that work on PSE for numerical domains either analyze programs with linear constraints, or develop novel techniques to handle solution counting of nonlinear constraints. For the string domain, however, previous work on PSE mainly focuses on efficient and accurate solution counting for automata-based string models and has not investigated whether a one-to-one relationship between the strings encoded by automata and input string values is preserved. In this work we demonstrate that traditional automata-based string models fail to maintain one-to-one relations and propose to use the weighted automata model, which preserves the one-to-one relation between the path constraint it encodes and the input string values. We use this model to implement a string constraint solver and show its correctness on a set of non-trivial synthetic benchmarks. We also present an empirical evaluation of traditional and proposed automata solvers on real-world string constraints. The evaluations show that while being less efficient than traditional automata models, the weighted automata model maintains correct solution counts.

关键词： quantitative program analysis probabilistic symbolic execution string constraints

来源：评论

学校读者我要写书评

暂无评论

What Is Decidable about string constraints with the ReplaceAll Function

引用

PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL 2018年第POPL期2卷 1–29页

作者： Chen, Taolue Chen, Yan Hague, Matthew Lin, Anthony W. Wu, Zhilin Birkbeck Univ London Dept Comp Sci & Informat Syst Malet St London WC1E 7HX England Chinese Acad Sci Inst Software State Key Lab Comp Sci Beijing Peoples R China Univ Chinese Acad Sci Beijing Peoples R China Royal Holloway Univ London Dept Comp Sci Egham Hill Egham TW20 0EX Surrey England Univ Oxford Dept Comp Sci Wolfson BuildinParks Rd Oxford OX1 3QD England

The theory of strings with concatenation has been widely argued as the basis of constraint solving for verifying string-manipulating programs. However, this theory is far from adequate for expressing many string constraints that are also needed in practice;for example, the use of regular constraints (pattern matching against a regular expression), and the string-replace function (replacing either the first occurrence or all occurrences of a "pattern" string constant/variable/regular expression by a "replacement" string constant/variable), among many others. Both regular constraints and the string-replace function are crucial for such applications as analysis of JavaScript (or more generally HTML5 applications) against cross-site scripting (XSS) vulnerabilities, which motivates us to consider a richer class of string constraints. The importance of the string-replace function (especially the replace-all facility) is increasingly recognised, which can be witnessed by the incorporation of the function in the input languages of several string constraint solvers. Recently, it was shown that any theory of strings containing the string-replace function (even the most restricted version where pattern/replacement strings are both constant strings) becomes undecidable if we do not impose some kind of straight-line (aka acyclicity) restriction on the formulas. Despite this, the straight-line restriction is still practically sensible since this condition is typically met by string constraints that are generated by symbolic execution. In this paper, we provide the first systematic study of straight-line string constraints with the string-replace function and the regular constraints as the basic operations. We show that a large class of such constraints (i.e. when only a constant string or a regular expression is permitted in the pattern) is decidable. We note that the string-replace function, even under this restriction, is sufficiently powerful for expressing the concatenation o

关键词： string constraints ReplaceAll Decision Procedures Constraint Solving Straight-Line Programs

来源：评论

学校读者我要写书评

暂无评论

A Uniform Framework for Handling Position constraints in string Solving

引用

Proceedings of the ACM on Programming Languages 2025年第PLDI期9卷 550-575页

作者： Yu-Fang Chen Vojtěch Havlena Michal Hečko Lukáš Holík Ondřej Lengál Academia Sinica Taipei Taiwan Brno University of Technology Brno Czech Republic Aalborg University Aalborg Denmark

We introduce a novel decision procedure for solving the class of position string constraints, which includes string disequalities, ¬prefixof, ¬suffixof, ***, and ¬***. These constraints are generated frequently in almost any application of string constraint solving. Our procedure avoids expensive encoding of the constraints to word equations and, instead, reduces the problem to checking conflicts on positions satisfying an integerconstraint obtained from the Parikh image of a polynomial-sized finite automaton with a special structure. By the reduction to counting, solving position constraints becomes NP-complete and for some cases even falls into PTime. This is much cheaper than the previously used techniques, which either used reductions generating word equations and length constraints (for which modern string solvers use exponential-space algorithms) or incomplete techniques. Our method is relevant especially for automata-based string solvers, which have recently achieved the best results in terms of practical efficiency, generality, and completeness guarantees. This work allows them to excel also on position constraints, which used to be their weakness. Besides the efficiency gains, we show that our framework may be extended to solve a large fragment of ¬contains (in NExpTime), for which decidability has been long open, and gives a hope to solve the general problem. Our implementation of the technique within the Z3-Noodler solver significantly improves its performance on position constraints.

关键词： SMT solving disequality length constraints monadic decomposition not contains regular languages stabilization string constraints word equations

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：