Publication Details
Efficient handling of string-number conversion
Atig Mohamed F. (Uppsala)
Bui Phi Diep (Uppsala)
Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT)
Chen Yu-Fang (ASIN)
Janků Petr, Ing. (DITS FIT BUT)
Lin Hsin-Hung (ASIN)
Wu Wei-Cheng (ASIN)
String Solver, Formal Verification, Automata
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.
@INPROCEEDINGS{FITPUB12452, author = "A. Parosh Abdulla and F. Mohamed Atig and Diep Phi Bui and Luk\'{a}\v{s} Hol\'{i}k and Yu-Fang Chen and Petr Jank\r{u} and Hsin-Hung Lin and Wei-Cheng Wu", title = "Efficient handling of string-number conversion", pages = "943--957", booktitle = "Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation", series = "Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)", year = 2020, location = "New York, US", publisher = "Association for Computing Machinery", ISBN = "978-1-4503-7613-6", doi = "10.1145/3385412.3386034", language = "english", url = "https://www.fit.vut.cz/research/publication/12452" }