- Computing and Information Systems - Research Publications
Computing and Information Systems - Research Publications
Permanent URI for this collection
5 results
Filters
Reset filtersSettings
Statistics
Citations
Search Results
Now showing
1 - 5 of 5
-
ItemAbstract Interpretation over Non-Lattice Abstract DomainsGange, G ; Navas, JA ; Schachte, P ; Søndergaard, H ; Stuckey, PJ ; Logozzo, F ; Fahndrich, M (Springer, 2013)The classical theoretical framework for static analysis of programs is abstract interpretation. Much of the power and elegance of that framework rests on the assumption that an abstract domain is a lattice. Nonetheless, and for good reason, the literature on program analysis provides many examples of non-lattice domains, including non-convex numeric domains. The lack of domain structure, however, has negative consequences, both for the precision of program analysis and for the termination of standard Kleene iteration. In this paper we explore these consequences and present general remedies.
-
ItemConstraint Programming for Dynamic Symbolic Execution of JavaScriptAmadini, 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.
-
ItemCombining String Abstract Domains for JavaScript Analysis: An EvaluationAmadini, 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.
-
ItemString constraint solving: past, present and futureAmadini, 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.
-
ItemAnalyzing Array Manipulating Programs by Program TransformationCornish, JRM ; Gange, G ; Navas, JA ; Schachte, P ; SONDERGAARD, H ; Stuckey, PJ ; Proietti, M ; Seki, H (Springer International Publishing, 2015)