Computing and Information Systems - Research Publications

Permanent URI for this collection

http://hdl.handle.net/11343/350

Filters

2017 - 2020 3
Reset filters

Settings
Statistics
Citations
Author: Amadini, Roberto × Author: Schachte, Peter × Author: Stuckey, Peter × Type: Conference Paper ×

Search Results

Now showing 1 - 3 of 3
  • Item
    Thumbnail Image
    Constraint Programming for Dynamic Symbolic Execution of JavaScript
    Amadini, R ; Andrlon, M ; Gange, G ; Schachte, P ; Søndergaard, H ; Stuckey, PJ ; Rousseau, LM ; Stergiou, K (Springer, 2019-01-01)
    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.
  • Item
    Thumbnail Image
    Combining String Abstract Domains for JavaScript Analysis: An Evaluation
    Amadini, R ; Jordan, A ; Gange, G ; Gauthier, F ; Schachte, P ; Sondergaard, H ; Stuckey, PJ ; Zhang, C ; Legay, A ; Margaria, T (SPRINGER INTERNATIONAL PUBLISHING AG, 2017-01-01)
    Strings play a central role in JavaScript and similar scripting languages. Owing to dynamic features such as the eval function and dynamic property access, precise string analysis is a prerequisite for automated reasoning about practically any kind of runtime property. Although the literature presents a considerable number of abstract domains for capturing and representing specific aspects of strings, we are not aware of tools that allow flexible combination of string abstract domains. Indeed, support for string analysis is often confined to a single, dedicated string domain. In this paper we describe a framework that allows us to combine multiple string abstract domains for the analysis of JavaScript programs. It is implemented as an extension of SAFE, an open-source static analysis tool. We investigate different combinations of abstract domains that capture various aspects of strings. Our evaluation suggests that a combination of a few, simple abstract domains suffice to outperform the precision of state-of-the-art static analysis tools for JavaScript.
  • Item
    Thumbnail Image
    String constraint solving: past, present and future
    Amadini, R ; Gange, G ; Schachte, P ; Sondergaard, H ; Stuckey, PJ ; DeGiacomo, G ; Catala, A ; Dilkina, B ; Milano, M ; Barro, S ; Bugarin, A ; Lang, J (University of Santiago de Compostela, 2020-01-01)
    String constraint solving is an important emerging field, given the ubiquity of strings over different fields such as formal analysis, automated testing, database query processing, and cybersecurity. This paper highlights the current state-of-the-art for string constraint solving, and identifies future challenges in this field.