Computing and Information Systems - Research Publications
Permanent URI for this collection
Search Results
1 - 10 of 11
-
ItemAbstract Interpretation over Non-Lattice Abstract Domains(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.
-
ItemDashed Strings and the Replace(-all) Constraint(Springer International Publishing, 2020)Dashed strings are a formalism for modelling the domain of string variables when solving combinatorial problems with string constraints. In this work we focus on (variants of) the Replace constraint, which aims to find the first occurrence of a query string in a target string, and (possibly) replaces it with a new string. We define a Replace propagator which can also handle Replace-Last (for replacing the last occurrence) and Replace-All (for replacing all the occurrences). Empirical results clearly show that string constraint solving can draw great benefit from this approach.
-
ItemA novel approach to string constraint solving(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.
-
ItemSweep-based propagation for string constraint solving(Association for the Advancement of Artificial Intelligence, 2018-01-01)Solving constraints over strings is an emerging important field. Recently, a Constraint Programming approach based on dashed strings has been proposed to enable a compact domain representation for potentially large bounded-length string variables. In this paper, we present a more efficient algorithm for propagating equality (and related constraints) over dashed strings. We call this propagation sweep-based. Experimental evidences show that sweep-based propagation is able to significantly outperform state-of-the-art approaches for string constraint solving.
-
ItemPropagating lex, find and replace with dashed strings(Springer International Publishing, 2018-01-01)Dashed strings have been recently proposed in Constraint Programming to represent the domain of string variables when solving combinatorial problems over strings. This approach showed promising performance on some classes of string problems, involving constraints like string equality and concatenation. However, there are a number of string constraints for which no propagator has yet been defined. In this paper, we show how to propagate lexicographic ordering (lex), find and replace with dashed strings. All of these are fundamental string operations: lex is the natural total order over strings, while find and replace are frequently used in string manipulation. We show that these propagators, that we implemented in G-Strings solver, allows us to be competitive with state-of-the-art approaches.
-
ItemPropagating Regular membership with dashed strings(Springer Nature, 2018-01-01)Using dashed strings is an approach recently introduced in Constraint Programming (CP) to represent the domain of string variables, when solving combinatorial problems with string constraints. One of the most important string constraints is that of regular membership: regular (x, R) imposes string x to be a member of the regular language defined by automaton R. The regular constraint is useful for specifying complex constraints on fixed length finite sequences, and regularly appears in CP models. Dealing with regular is also desirable in software testing and verification, because regular expressions are often used in modern programming languages for pattern matching. In this paper, we define a regular propagator for dashed string solvers. We show that this propagator, implemented in the G-Strings solver, is substantially better than the current state-of-the-art. We also demonstrate that many regular constraints appearing in string solving benchmarks can actually be tackled by dashed strings solvers without explicitly using REGULAR.
-
ItemConstraint Programming for Dynamic Symbolic Execution of JavaScript(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 Evaluation(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 future(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.
-
ItemConstraint propagation and explanation over novel types by abstract compilation(Schloss Dagstuhl, 2016-11-01)© Graeme Gange and Peter J. Stuckey. The appeal of constraint programming (CP) lies in compositionality - the ability to mix and match constraints as needed. However, this flexibility typically does not extend to the types of variables. Solvers usually support only a small set of pre-defined variable types, and extending this is not typically a simple exercise: not only must the solver engine be updated, but then the library of supported constraints must be re-implemented to support the new type. In this paper, we attempt to ease this second step. We describe a system for automatically deriving a native-code implementation of a global constraint (over novel variable types) from a declarative specification, complete with the ability to explain its propagation, a requirement if we want to make use of modern lazy clause generation CP solvers. We demonstrate this approach by adding support for wrapped-integer variables to chuffed, a lazy clause generation CP solver.