@inproceedings{Ama-And-Gan-Sch-Son-Stu_CPAIOR19,
  author    = {Roberto Amadini and 
		Mak Andrlon and 
		Graeme Gange and 
		Peter Schachte and 
		Harald S{\o}ndergaard and 
		Peter J. Stuckey},
  title     = {Constraint Programming for Dynamic Symbolic Execution of
                {JavaScript}},
  editor    = {L.-M. Rousseau and K. Stergiou},
  booktitle = {Integration of Constraint Programming, Artificial Intelligence,
		and Operations Research: Proceedings of the 16th International
		Conference (CPAIOR 2019)},
  series    = {Lecture Notes in Computer Science},
  volume    = {11494}, 
  pages     = {1--19},
  year      = {2019},
  doi       = {10.1007/978-3-030-19212-9_1},
  url_Paper = {https://minerva-access.unimelb.edu.au/rest/bitstreams/b999c802-90f6-5ce4-8b79-c298bfc62afa/retrieve},
  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 \textsc{Aratha}. We use \textsc{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.},
  keywords  = {Symbolic execution, Constraint programming, String solvers, JavaScript},
}

{"_id":"YCxG4CaiJ3abfEthJ","bibbaseid":"amadini-andrlon-gange-schachte-sndergaard-stuckey-constraintprogrammingfordynamicsymbolicexecutionofjavascript-2019","author_short":["Amadini, R.","Andrlon, M.","Gange, G.","Schachte, P.","Søndergaard, H.","Stuckey, P. J."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"firstnames":["Roberto"],"propositions":[],"lastnames":["Amadini"],"suffixes":[]},{"firstnames":["Mak"],"propositions":[],"lastnames":["Andrlon"],"suffixes":[]},{"firstnames":["Graeme"],"propositions":[],"lastnames":["Gange"],"suffixes":[]},{"firstnames":["Peter"],"propositions":[],"lastnames":["Schachte"],"suffixes":[]},{"firstnames":["Harald"],"propositions":[],"lastnames":["Søndergaard"],"suffixes":[]},{"firstnames":["Peter","J."],"propositions":[],"lastnames":["Stuckey"],"suffixes":[]}],"title":"Constraint Programming for Dynamic Symbolic Execution of JavaScript","editor":[{"firstnames":["L.-M."],"propositions":[],"lastnames":["Rousseau"],"suffixes":[]},{"firstnames":["K."],"propositions":[],"lastnames":["Stergiou"],"suffixes":[]}],"booktitle":"Integration of Constraint Programming, Artificial Intelligence, and Operations Research: Proceedings of the 16th International Conference (CPAIOR 2019)","series":"Lecture Notes in Computer Science","volume":"11494","pages":"1–19","year":"2019","doi":"10.1007/978-3-030-19212-9_1","url_paper":"https://minerva-access.unimelb.edu.au/rest/bitstreams/b999c802-90f6-5ce4-8b79-c298bfc62afa/retrieve","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 \\textscAratha. We use \\textscG-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.","keywords":"Symbolic execution, Constraint programming, String solvers, JavaScript","bibtex":"@inproceedings{Ama-And-Gan-Sch-Son-Stu_CPAIOR19,\n author = {Roberto Amadini and \n\t\tMak Andrlon and \n\t\tGraeme Gange and \n\t\tPeter Schachte and \n\t\tHarald S{\\o}ndergaard and \n\t\tPeter J. Stuckey},\n title = {Constraint Programming for Dynamic Symbolic Execution of\n {JavaScript}},\n editor = {L.-M. Rousseau and K. Stergiou},\n booktitle = {Integration of Constraint Programming, Artificial Intelligence,\n\t\tand Operations Research: Proceedings of the 16th International\n\t\tConference (CPAIOR 2019)},\n series = {Lecture Notes in Computer Science},\n volume = {11494}, \n pages = {1--19},\n year = {2019},\n doi = {10.1007/978-3-030-19212-9_1},\n url_Paper = {https://minerva-access.unimelb.edu.au/rest/bitstreams/b999c802-90f6-5ce4-8b79-c298bfc62afa/retrieve},\n abstract = {Dynamic Symbolic Execution (DSE) combines concrete and symbolic \n\t\texecution, usually for the purpose of generating good test \n\t\tsuites automatically. It relies on constraint solvers to solve\n\t\tpath conditions and to generate new inputs to explore. DSE \n\t\ttools usually make use of SMT solvers for constraint solving.\n\t\tIn this paper, we show that constraint programming (CP) is a\n\t\tpowerful alternative or complementary technique for DSE.\n\t\tSpecifically, we apply CP techniques for DSE of JavaScript, the\n\t\tde facto standard for web programming. We capture the JavaScript\n\t\tsemantics with MiniZinc and integrate this approach into a tool\n\t\twe call \\textsc{Aratha}. We use \\textsc{G-Strings}, a CP solver\n\t\tequipped with string variables, for solving path conditions, \n\t\tand we compare the performance of this approach against \n\t\tstate-of-the-art SMT solvers. Experimental results, in terms of\n\t\tboth speed and coverage, show the benefits of our approach,\n\t\tthus opening new research vistas for using CP techniques in \n\t\tthe service of program analysis.},\n keywords = {Symbolic execution, Constraint programming, String solvers, JavaScript},\n}\n\n","author_short":["Amadini, R.","Andrlon, M.","Gange, G.","Schachte, P.","Søndergaard, H.","Stuckey, P. J."],"editor_short":["Rousseau, L.","Stergiou, K."],"key":"Ama-And-Gan-Sch-Son-Stu_CPAIOR19","id":"Ama-And-Gan-Sch-Son-Stu_CPAIOR19","bibbaseid":"amadini-andrlon-gange-schachte-sndergaard-stuckey-constraintprogrammingfordynamicsymbolicexecutionofjavascript-2019","role":"author","urls":{" paper":"https://minerva-access.unimelb.edu.au/rest/bitstreams/b999c802-90f6-5ce4-8b79-c298bfc62afa/retrieve"},"keyword":["Symbolic execution","Constraint programming","String solvers","JavaScript"],"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"people.eng.unimelb.edu.au/harald/bibbase.bib","dataSources":["yWvm3kzg5vKQAPLm7","ofmsZryxNDBSpE7j5","9aC4cxLD8D6oJ3FLN","wpkuJrZJJtqra3FbL","XqcrNTrCCBr9mSd37","W7ih7WyQivP4EDh83"],"keywords":["symbolic execution","constraint programming","string solvers","javascript"],"search_terms":["constraint","programming","dynamic","symbolic","execution","javascript","amadini","andrlon","gange","schachte","søndergaard","stuckey"],"title":"Constraint Programming for Dynamic Symbolic Execution of JavaScript","year":2019}