zbMATH — the first resource for mathematics

Constraint programming for dynamic symbolic execution of JavaScript. (English) Zbl 07116682
Rousseau, Louis-Martin (ed.) et al., Integration of constraint programming, artificial intelligence, and operations research. 16th international conference, CPAIOR 2019, Thessaloniki, Greece, June 4–7, 2019. Proceedings. Cham: Springer (ISBN 978-3-030-19211-2/pbk; 978-3-030-19212-9/ebook). Lecture Notes in Computer Science 11494, 1-19 (2019).
Summary: Dynamic Symbolic Execution (DSE) combines concrete and symbolic execution, usually for the purpose of generating good test suites automatically. It relies on constraint solvers to solve path conditions and to generate new inputs to explore. DSE tools usually make use of SMT solvers for constraint solving. In this paper, we show that constraint programming (CP) is a powerful alternative or complementary technique for DSE. Specifically, we apply CP techniques for DSE of JavaScript, the de facto standard for web programming. We capture the JavaScript semantics with MiniZinc and integrate this approach into a tool we call Aratha. We use G-Strings, a CP solver equipped with string variables, for solving path conditions, and we compare the performance of this approach against state-of-the-art SMT solvers. Experimental results, in terms of both speed and coverage, show the benefits of our approach, thus opening new research vistas for using CP techniques in the service of program analysis.
For the entire collection see [Zbl 1410.68020].
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
90C27 Combinatorial optimization
Full Text: DOI