Detail výsledku
Efficient handling of string-number conversion
Janků Petr, Ing., Ph.D.
BUI PHI, D.
Chen Yu-Fang
LIN, H.
WU, W.
Abdulla Parosh
Atig Mohamed, FIT (FIT)
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.
String Solver, Formal Verification, Automata
@inproceedings{BUT169183,
author="HOLÍK, L. and JANKŮ, P. and BUI PHI, D. and CHEN, Y. and LIN, H. and WU, W. and ABDULLA, P. and ATIG, M.",
title="Efficient handling of string-number conversion",
booktitle="Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation",
year="2020",
series="Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)",
pages="943--957",
publisher="Association for Computing Machinery",
address="New York",
doi="10.1145/3385412.3386034",
isbn="978-1-4503-7613-6",
url="https://dl.acm.org/doi/10.1145/3385412.3386034"
}IT4Innovations excellence in science, MŠMT, Národní program udržitelnosti II, LQ1602, zahájení: 2016-01-01, ukončení: 2020-12-31, ukončen
Spolehlivé, bezpečné a efektivní počítačové systémy, VUT, Vnitřní projekty VUT, FIT-S-20-6427, zahájení: 2020-03-01, ukončení: 2023-02-28, ukončen