Computing and Information Systems - Research Publications

Permanent URI for this collection

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

Filters

2017 3
Reset filters

Settings
Statistics
Citations
Start date: 2017 × End date: 2017 × Type: Conference Paper × Author: Amadini, Roberto ×

Search Results

Now showing 1 - 3 of 3
  • Item
    Thumbnail Image
    A novel approach to string constraint solving
    Amadini, R ; Gange, G ; Stuckey, PJ ; Tack, G ; Beck, JC (Springer, 2017-01-01)
    String processing is ubiquitous across computer science, and arguably more so in web programming. In order to reason about programs manipulating strings we need to solve constraints over strings. In Constraint Programming, the only approaches we are aware for representing string variables—having bounded yet possibly unknown size—degrade when the maximum possible string length becomes too large. In this paper, we introduce a novel approach that decouples the size of the string representation from its maximum length. The domain of a string variable is dynamically represented by a simplified regular expression that we called a dashed string, and the constraint solving relies on propagation of information based on equations between dashed strings. We implemented this approach in G-Strings, a new string solver—built on top of Gecode solver—that already shows some promising results.
  • Item
    Thumbnail Image
    MiniZinc with Strings
    Amadini, R ; Flener, P ; Pearson, J ; Scott, JD ; Stuckey, PJ ; Tack, G ; Hermenegildo, MV ; LopezGarcia, P (SPRINGER INTERNATIONAL PUBLISHING AG, 2017-01-01)
    Strings are extensively used in modern programming languages and constraints over strings of unknown length occur in a wide range of real-world applications such as software analysis and verification, testing, model checking, and web security. Nevertheless, practically no constraint programming solver natively supports string constraints. We introduce string variables and a suitable set of string constraints as builtin features of the MiniZinc modelling language. Furthermore, we define an interpreter for converting a MiniZinc model with strings into a FlatZinc instance relying only on integer variables. This conversion is obtained via rewrite rules, and does not require any extension of the existing FlatZinc specification. This provides a user-friendly interface for modelling combinatorial problems with strings, and enables both string and non-string solvers to actually solve such problems.
  • 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.