Constraint programming for dynamic symbolic execution of JavaScript

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

doi:10.1007/978-3-030-19212-9_1

Constraint programming for dynamic symbolic execution of JavaScript

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

Department of Data Science & AI

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › Research › peer-review

8 Citations (Scopus)

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 language	English
Title of host publication	Integration of Constraint Programming, Artificial Intelligence, and Operations Research
Subtitle of host publication	16th International Conference, CPAIOR 2019 Thessaloniki, Greece, June 4–7, 2019 Proceedings
Editors	Louis-Martin Rousseau, Kostas Stergiou
Place of Publication	Cham Switzerland
Publisher	Springer
Pages	1-19
Number of pages	19
ISBN (Electronic)	9783030192129
ISBN (Print)	9783030192112
DOIs	https://doi.org/10.1007/978-3-030-19212-9_1
Publication status	Published - 2019
Event	International Conference on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming for Combinatorial Optimization Problems 2019 - Thessaloniki, Greece Duration: 4 Jun 2019 → 7 Jun 2019 Conference number: 16th https://cpaior2019.uowm.gr/ (Conference website) https://link.springer.com/book/10.1007/978-3-030-19212-9 (Proceedings)

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	11494
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	International Conference on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming for Combinatorial Optimization Problems 2019
Abbreviated title	CPAIOR 2019
Country/Territory	Greece
City	Thessaloniki
Period	4/06/19 → 7/06/19
Internet address	https://cpaior2019.uowm.gr/ (Conference website) https://link.springer.com/book/10.1007/978-3-030-19212-9 (Proceedings)

Access to Document

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

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 ). Springer. https://doi.org/10.1007/978-3-030-19212-9_1

Amadini, Roberto ; Andrlon, Mak ; Gange, Graeme et al. / 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",

note = "International Conference on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming for Combinatorial Optimization Problems 2019<br/>, CPAIOR 2019 ; Conference date: 04-06-2019 Through 07-06-2019",

url = "https://cpaior2019.uowm.gr/, https://link.springer.com/book/10.1007/978-3-030-19212-9",

}

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 et al.
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 proceeding › Conference Paper › Research › peer-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.

N1 - Conference code: 16th

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

AN - SCOPUS:85066823236

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

T2 - International Conference on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming for Combinatorial Optimization Problems 2019<br/>

Y2 - 4 June 2019 through 7 June 2019

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 ). doi: 10.1007/978-3-030-19212-9_1

Constraint programming for dynamic symbolic execution of JavaScript

Abstract

Publication series

Conference

Access to Document

Other files and links

Towards reliability in combinatorial optimisation

Cite this

Constraint programming for dynamic symbolic execution of JavaScript

Abstract

Publication series

Conference

Access to Document

Other files and links

Projects

Towards reliability in combinatorial optimisation

Cite this