Constraint programming for dynamic symbolic execution of JavaScript

Roberto Amadini, Mak Andrlon, Graeme Gange, Peter Schachte, Harald Søndergaard, Peter J. Stuckey

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

Abstract

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.

Original languageEnglish
Title of host publicationIntegration of Constraint Programming, Artificial Intelligence, and Operations Research
Subtitle of host publication16th International Conference, CPAIOR 2019 Thessaloniki, Greece, June 4–7, 2019 Proceedings
EditorsLouis-Martin Rousseau, Kostas Stergiou
Place of PublicationCham Switzerland
PublisherSpringer
Pages1-19
Number of pages19
ISBN (Electronic)9783030192129
ISBN (Print)9783030192112
DOIs
Publication statusPublished - 2019
EventInternational Conference on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming for Combinatorial Optimization Problems 2019
- Thessaloniki, Greece
Duration: 4 Jun 20197 Jun 2019
Conference number: 16th
https://cpaior2019.uowm.gr/

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume11494
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceInternational Conference on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming for Combinatorial Optimization Problems 2019
Abbreviated titleCPAIOR 2019
CountryGreece
CityThessaloniki
Period4/06/197/06/19
Internet address

Cite this

Amadini, R., Andrlon, M., Gange, G., Schachte, P., Søndergaard, H., & Stuckey, P. J. (2019). Constraint programming for dynamic symbolic execution of JavaScript. In L-M. Rousseau, & K. Stergiou (Eds.), Integration of Constraint Programming, Artificial Intelligence, and Operations Research: 16th International Conference, CPAIOR 2019 Thessaloniki, Greece, June 4–7, 2019 Proceedings (pp. 1-19). (Lecture Notes in Computer Science ; Vol. 11494 ). Cham Switzerland: Springer. https://doi.org/10.1007/978-3-030-19212-9_1
Amadini, Roberto ; Andrlon, Mak ; Gange, Graeme ; Schachte, Peter ; Søndergaard, Harald ; Stuckey, Peter J. / Constraint programming for dynamic symbolic execution of JavaScript. Integration of Constraint Programming, Artificial Intelligence, and Operations Research: 16th International Conference, CPAIOR 2019 Thessaloniki, Greece, June 4–7, 2019 Proceedings. editor / Louis-Martin Rousseau ; Kostas Stergiou. Cham Switzerland : Springer, 2019. pp. 1-19 (Lecture Notes in Computer Science ).
@inproceedings{452b31f847fb4cf0a41b890afdb7f861,
title = "Constraint programming for dynamic symbolic execution of JavaScript",
abstract = "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.",
author = "Roberto Amadini and Mak Andrlon and Graeme Gange and Peter Schachte and Harald S{\o}ndergaard and Stuckey, {Peter J.}",
year = "2019",
doi = "10.1007/978-3-030-19212-9_1",
language = "English",
isbn = "9783030192112",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "1--19",
editor = "Louis-Martin Rousseau and Kostas Stergiou",
booktitle = "Integration of Constraint Programming, Artificial Intelligence, and Operations Research",

}

Amadini, R, Andrlon, M, Gange, G, Schachte, P, Søndergaard, H & Stuckey, PJ 2019, Constraint programming for dynamic symbolic execution of JavaScript. in L-M Rousseau & K Stergiou (eds), Integration of Constraint Programming, Artificial Intelligence, and Operations Research: 16th International Conference, CPAIOR 2019 Thessaloniki, Greece, June 4–7, 2019 Proceedings. Lecture Notes in Computer Science , vol. 11494 , Springer, Cham Switzerland, pp. 1-19, International Conference on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming for Combinatorial Optimization Problems 2019
, Thessaloniki, Greece, 4/06/19. https://doi.org/10.1007/978-3-030-19212-9_1

Constraint programming for dynamic symbolic execution of JavaScript. / Amadini, Roberto; Andrlon, Mak; Gange, Graeme; Schachte, Peter; Søndergaard, Harald; Stuckey, Peter J.

Integration of Constraint Programming, Artificial Intelligence, and Operations Research: 16th International Conference, CPAIOR 2019 Thessaloniki, Greece, June 4–7, 2019 Proceedings. ed. / Louis-Martin Rousseau; Kostas Stergiou. Cham Switzerland : Springer, 2019. p. 1-19 (Lecture Notes in Computer Science ; Vol. 11494 ).

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

TY - GEN

T1 - Constraint programming for dynamic symbolic execution of JavaScript

AU - Amadini, Roberto

AU - Andrlon, Mak

AU - Gange, Graeme

AU - Schachte, Peter

AU - Søndergaard, Harald

AU - Stuckey, Peter J.

PY - 2019

Y1 - 2019

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85066823236&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-19212-9_1

DO - 10.1007/978-3-030-19212-9_1

M3 - Conference Paper

SN - 9783030192112

T3 - Lecture Notes in Computer Science

SP - 1

EP - 19

BT - Integration of Constraint Programming, Artificial Intelligence, and Operations Research

A2 - Rousseau, Louis-Martin

A2 - Stergiou, Kostas

PB - Springer

CY - Cham Switzerland

ER -

Amadini R, Andrlon M, Gange G, Schachte P, Søndergaard H, Stuckey PJ. Constraint programming for dynamic symbolic execution of JavaScript. In Rousseau L-M, Stergiou K, editors, Integration of Constraint Programming, Artificial Intelligence, and Operations Research: 16th International Conference, CPAIOR 2019 Thessaloniki, Greece, June 4–7, 2019 Proceedings. Cham Switzerland: Springer. 2019. p. 1-19. (Lecture Notes in Computer Science ). https://doi.org/10.1007/978-3-030-19212-9_1