Sound regular expression semantics for dynamic symbolic execution of JavaScript. / Loring, Blake; Mitchell, Duncan; Kinder, Johannes.

PLDI'19: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, 2019. p. 425-438.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Published

Standard

Sound regular expression semantics for dynamic symbolic execution of JavaScript. / Loring, Blake; Mitchell, Duncan; Kinder, Johannes.

PLDI'19: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, 2019. p. 425-438.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Harvard

Loring, B, Mitchell, D & Kinder, J 2019, Sound regular expression semantics for dynamic symbolic execution of JavaScript. in PLDI'19: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, pp. 425-438, 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, Phoenix, United States, 24/06/19. https://doi.org/10.1145/3314221.3314645

APA

Loring, B., Mitchell, D., & Kinder, J. (2019). Sound regular expression semantics for dynamic symbolic execution of JavaScript. In PLDI'19: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (pp. 425-438). ACM. https://doi.org/10.1145/3314221.3314645

Vancouver

Loring B, Mitchell D, Kinder J. Sound regular expression semantics for dynamic symbolic execution of JavaScript. In PLDI'19: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM. 2019. p. 425-438 https://doi.org/10.1145/3314221.3314645

Author

Loring, Blake ; Mitchell, Duncan ; Kinder, Johannes. / Sound regular expression semantics for dynamic symbolic execution of JavaScript. PLDI'19: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, 2019. pp. 425-438

BibTeX

@inproceedings{a18f2ca3150b484fb7923ac88155fe2d,
title = "Sound regular expression semantics for dynamic symbolic execution of JavaScript",
abstract = "Support for regular expressions in symbolic execution-based tools for test generation and bug finding is insufficient. Common aspects of mainstream regular expression engines, such as backreferences or greedy matching, are ignored or imprecisely approximated, leading to poor test coverage or missed bugs. In this paper, we present a model for the complete regular expression language of ECMAScript 2015 (ES6), which is sound for dynamic symbolic execution of the test and exec functions. We model regular expression operations using string constraints and classical regular expressions and use a refinement scheme to address the problem of matching precedence and greediness. We implemented our model in ExpoSE, a dynamic symbolic execution engine for JavaScript, and evaluated it on over 1,000 Node.js packages containing regular expressions, demonstrating that the strategy is effective and can significantly increase the number of successful regular expression queries and therefore boost coverage.",
author = "Blake Loring and Duncan Mitchell and Johannes Kinder",
year = "2019",
month = "6",
day = "8",
doi = "10.1145/3314221.3314645",
language = "English",
pages = "425--438",
booktitle = "PLDI'19",
publisher = "ACM",

}

RIS

TY - GEN

T1 - Sound regular expression semantics for dynamic symbolic execution of JavaScript

AU - Loring, Blake

AU - Mitchell, Duncan

AU - Kinder, Johannes

PY - 2019/6/8

Y1 - 2019/6/8

N2 - Support for regular expressions in symbolic execution-based tools for test generation and bug finding is insufficient. Common aspects of mainstream regular expression engines, such as backreferences or greedy matching, are ignored or imprecisely approximated, leading to poor test coverage or missed bugs. In this paper, we present a model for the complete regular expression language of ECMAScript 2015 (ES6), which is sound for dynamic symbolic execution of the test and exec functions. We model regular expression operations using string constraints and classical regular expressions and use a refinement scheme to address the problem of matching precedence and greediness. We implemented our model in ExpoSE, a dynamic symbolic execution engine for JavaScript, and evaluated it on over 1,000 Node.js packages containing regular expressions, demonstrating that the strategy is effective and can significantly increase the number of successful regular expression queries and therefore boost coverage.

AB - Support for regular expressions in symbolic execution-based tools for test generation and bug finding is insufficient. Common aspects of mainstream regular expression engines, such as backreferences or greedy matching, are ignored or imprecisely approximated, leading to poor test coverage or missed bugs. In this paper, we present a model for the complete regular expression language of ECMAScript 2015 (ES6), which is sound for dynamic symbolic execution of the test and exec functions. We model regular expression operations using string constraints and classical regular expressions and use a refinement scheme to address the problem of matching precedence and greediness. We implemented our model in ExpoSE, a dynamic symbolic execution engine for JavaScript, and evaluated it on over 1,000 Node.js packages containing regular expressions, demonstrating that the strategy is effective and can significantly increase the number of successful regular expression queries and therefore boost coverage.

U2 - 10.1145/3314221.3314645

DO - 10.1145/3314221.3314645

M3 - Conference contribution

SP - 425

EP - 438

BT - PLDI'19

PB - ACM

ER -