Sökning: WFRF:(Lin Hu)
> (2020-2024) >
Solving String Cons...
Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and Variables
-
- Chen, Taolue (författare)
- Birkbeck Univ London, Dept Comp Sci, Malet St, London, England.
-
- Flores-Lamas, Alejandro (författare)
- Royal Holloway Univ London, Dept Comp Sci, Egham Hill, Egham TW20 0EX, Surrey, England.
-
- Hague, Matthew (författare)
- Royal Holloway Univ London, Dept Comp Sci, Egham Hill, Egham TW20 0EX, Surrey, England.
-
visa fler...
-
- Han, Zhilei (författare)
- Tsinghua Univ, Sch Software, Beijing, Peoples R China.
-
- Hu, Denghang (författare)
- Chinese Acad Sci, Inst Software, State Key Lab Comp Sci, Beijing, Peoples R China.;Univ Chinese Acad Sci, Beijing, Peoples R China.
-
- Kan, Shuanglong (författare)
- Univ Kaiserslautern, Kaiserslautern, Germany.
-
- Lin, Anthony W. (författare)
- Univ Kaiserslautern, Kaiserslautern, Germany.;Max Planck Inst, Kaiserslautern, Germany.
-
- Rümmer, Philipp, 1978- (författare)
- Uppsala universitet,Datorteknik
-
- Wu, Zhilin (författare)
- Chinese Acad Sci, Inst Software, State Key Lab Comp Sci, Beijing, Peoples R China.;Univ Chinese Acad Sci, Beijing, Peoples R China.
-
visa färre...
-
Birkbeck Univ London, Dept Comp Sci, Malet St, London, England Royal Holloway Univ London, Dept Comp Sci, Egham Hill, Egham TW20 0EX, Surrey, England. (creator_code:org_t)
- 2022-01-12
- 2022
- Engelska.
-
Ingår i: Proceedings of the ACM on Programming Languages. - : Association for Computing Machinery (ACM). - 2475-1421. ; 6
- Relaterad länk:
-
https://doi.org/10.1...
-
visa fler...
-
https://uu.diva-port... (primary) (Raw object)
-
https://dl.acm.org/d...
-
https://urn.kb.se/re...
-
https://doi.org/10.1...
-
visa färre...
Abstract
Ämnesord
Stäng
- Regular expressions are a classical concept in formal language theory. Regular expressions in programming languages (RegEx) such as JavaScript, feature non-standard semantics of operators (e.g. greedy/lazy Kleene star), as well as additional features such as capturing groups and references. While symbolic execution of programs containing RegExes appeals to string solvers natively supporting important features of RegEx, such a string solver is hitherto missing. In this paper, we propose the first string theory and string solver that natively provides such support. The key idea of our string solver is to introduce a new automata model, called prioritized streaming string transducers (PSST), to formalize the semantics of RegEx-dependent string functions. PSSTs combine priorities, which have previously been introduced in prioritized finite-state automata to capture greedy/lazy semantics, with string variables as in streaming string transducers to model capturing groups. We validate the consistency of the formal semantics with the actual JavaScript semantics by extensive experiments. Furthermore, to solve the string constraints, we show that PSSTs enjoy nice closure and algorithmic properties, in particular, the regularity-preserving property (i.e., pre-images of regular constraints under PSSTs are regular), and introduce a sound sequent calculus that exploits these properties and performs propagation of regular constraints by means of taking post-images or pre-images. Although the satisfiability of the string constraint language is generally undecidable, we show that our approach is complete for the so-called straightline fragment. We evaluate the performance of our string solver on over 195 000 string constraints generated from an open-source RegEx library. The experimental results show the efficacy of our approach, drastically improving the existing methods (via symbolic execution) in both precision and efficiency.
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
Nyckelord
- String Constraint Solving
- Regular Expressions
- Transducers
- Symbolic Execution
Publikations- och innehållstyp
- ref (ämneskategori)
- art (ämneskategori)
Hitta via bibliotek
Till lärosätets databas
- Av författaren/redakt...
-
Chen, Taolue
-
Flores-Lamas, Al ...
-
Hague, Matthew
-
Han, Zhilei
-
Hu, Denghang
-
Kan, Shuanglong
-
visa fler...
-
Lin, Anthony W.
-
Rümmer, Philipp, ...
-
Wu, Zhilin
-
visa färre...
- Om ämnet
-
- NATURVETENSKAP
-
NATURVETENSKAP
-
och Data och informa ...
-
och Datavetenskap
- Artiklar i publikationen
-
Proceedings of t ...
- Av lärosätet
-
Uppsala universitet