Efficient handling of string-number conversion
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Julian Dolby, Petr Janku, Hsin-Hung Lin, Lukás Holík, Wei-Cheng Wu
Abstract
String-number conversion is an important class of constraints needed for the symbolic execution of string-manipulating programs. In particular solving string constraints with string-number conversion is necessary for the analysis of scripting languages such as JavaScript and Python, where string-number conversion is a part of the definition of the core semantics of these languages. However, solving this type of constraint is very challenging for the state-of-the-art solvers. We propose in this paper an approach that can efficiently support both string-number conversion and other common types of string constraints. Experimental results show that it significantly outperforms other state-of-the-art tools on benchmarks that involves string-number conversion.
Ask about this paper
Ask your agent about it.
Lune has read the top-tier papers around this one, so every answer names the papers it rests on.
Your agent calls
Lunesearch_papers
Free to start. No credit card required.
Terminal
Install the CLIlune papers get eff0e10c-89c4-430c-ac48-c496dd6d80c5Cited by top-tier papers3
- An SMT Solver for Regular Expressions and Linear Arithmetic over String LengthMurphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea et al.CAV 2021 · 37 citations
- Word Equations in Synergy with Regular ConstraintsFrantisek Blahoudek, Yu-Fang Chen, David Chocholatý, Vojtech Havlena et al.FM 2023 · 16 citations
- Optimization Modulo Integer Linear-Exponential ProgramsS. Hitarth, Alessio Mansutti, Guruprerana ShabadiSODA 2026
Related papers
- Solving string constraints with Regex-dependent functions through transducers with priorities and variablesTaolue Chen, Alejandro Flores-Lamas, Matthew Hague, Zhilei Han et al.POPL 2022 · 39 citations
- Neuro-Symbolic Execution: Augmenting Symbolic Execution with Neural ConstraintsShiqi Shen, Shweta Shinde, Soundarya Ramesh, Abhik Roychoudhury et al.NDSS 2019 · 43 citations
- Inter-theory dependency analysis for SMT string solversMinh-Thai Trinh, Duc-Hiep Chu, Joxan JaffarOOPSLA 2020 · 5 citations
- Multiplex Symbolic Execution: Exploring Multiple Paths by Solving OnceYufeng Zhang, Zhenbang Chen, Ziqi Shuai, Tianqi Zhang et al.ASE 2020 · 17 citations
- Boosting symbolic execution via constraint solving time prediction (experience paper)Sicheng Luo, Hui Xu, Yanxiang Bi, Xin Wang et al.ISSTA 2021 · 12 citations
