Author name cluster
Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.
LOPSTR Conference 2021 Conference Paper
Abstract We survey recent developments in string static analysis, with an emphasis on how string abstract domains can be combined. The paper has formed the basis for an invited presentation given to LOPSTR 2021 and PPDP 2021.
LOPSTR Conference 2020 Conference Paper
Abstract Given a portfolio of algorithms, the goal of Algorithm Selection ( AS ) is to select the best algorithm(s) for a new, unseen problem instance. Dynamic Symbolic Execution ( DSE ) brings together concrete and symbolic execution to maximise the program coverage. DSE uses a constraint solver to solve the path conditions and generate new inputs to explore. In this paper we join these lines of research by introducing a model that combines DSE and AS approaches. The proposed AS/DSE model is a generic and flexible framework enabling the DSE engine to solve the path conditions it collects with a portfolio of different solvers, by exploiting and extending the well-known AS techniques that have been developed over the last decade. In this way, one can increase the coverage and sometimes even outperform the aggregate coverage achievable by running simultaneously all the solvers of the portfolio.
ECAI Conference 2020 Conference Paper
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.
SAT Conference 2017 Conference Paper
Abstract Verification tasks frequently require deciding systems of linear constraints over modular (machine) arithmetic. Existing approaches for reasoning over modular arithmetic use bit-vector solvers, or else approximate machine integers with mathematical integers and use arithmetic solvers. Neither is ideal; the first is sound but inefficient, and the second is efficient but unsound. We describe a linear encoding which correctly describes modular arithmetic semantics, yielding an optimistic but sound approach. Our method abstracts the problem with linear arithmetic, but progressively refines the abstraction when modular semantics is violated. This preserves soundness while exploiting the mostly integer nature of the constraint problem. We present a prototype implementation, which gives encouraging experimental results.
TCS Journal 2016 Journal Article
Often, when analyzing the behaviour of systems modelled as context-free languages, we wish to know if two languages overlap. To this end, we present a class of semi-decision procedures for regular separability of context-free languages, based on counter-example guided abstraction refinement. We propose two effective instances of this approach, one that is complete but relatively expensive, and one that is inexpensive and sound, but for which we do not have a completeness proof. The complete method will prove disjointness whenever the input languages are regularly separable. Both methods will terminate whenever the input languages overlap. We provide an experimental evaluation of these procedures, and demonstrate their practicality on a range of verification and language-theoretic instances.
LOPSTR Conference 2014 Conference Paper
Abstract We explore a transformational approach to the problem of verifying simple array-manipulating programs. Traditionally, verification of such programs requires intricate analysis machinery to reason with universally quantified statements about symbolic array segments, such as “every data item stored in the segment A[i] to A[j] is equal to the corresponding item stored in the segment B[i] to B[j]. ” We define a simple abstract machine which allows for set-valued variables and we show how to translate programs with array operations to array-free code for this machine. For the purpose of program analysis, the translated program remains faithful to the semantics of array manipulation. Based on our implementation in LLVM, we evaluate the approach with respect to its ability to extract useful invariants and the cost in terms of code size.
ICAPS Conference 2014 Conference Paper
We introduce a novel algorithm for temporal planning in Golog using shared resources, and describe the Bulk Freight Rail Scheduling Problem, a motivating example of such a temporal domain. We use the framework of column generation to tackle complex resource constrained temporal planning problems that are beyond the scope of current planning technology by combining: the global view of a linear programming relaxation of the problem; the strength of search infinding action sequences; and the domain knowledge that can be encoded in a Golog program. We show that our approach significantly outperforms state-of-the-art temporal planning and constraint programming approaches in this domain, in addition to existing temporal Golog implementations. We also apply our algorithm to a temporal variant of blocks-world where our decomposition speeds proof of optimality significantly compared to other anytime algorithms. We discuss the potential of the underlying algorithm being applicable to STRIPS planning, with further work.
AIJ Journal 2010 Journal Article
Since Selman and Kautz's seminal work on the use of Horn approximation to speed up the querying of knowledge bases, there has been great interest in Boolean approximation for AI applications. There are several Boolean classes with desirable computational properties similar to those of the Horn class. The class of affine Boolean functions, for example, has been proposed as an interesting alternative to Horn for knowledge compilation. To investigate the trade-offs between precision and efficiency in knowledge compilation, we compare, analytically and empirically, four well-known Boolean classes, and their combinations, for ability to preserve information. We note that traditional evaluation which explores unit-clause consequences of random hard 3-CNF formulas does not tell the full story, and we complement that evaluation with experiments based on a variety of assumptions about queries and the underlying knowledge base.
LOPSTR Conference 1990 Conference Paper
Abstract It has become popular to express dataflow analyses in logical form. In this paper we investigate a new approach to the analysis of functional programs, based on synthesis of constraint logic programs. We sketch how the language Toupie, originally designed with logic program analysis as one objective, lends itself also to sophisticated strictness analysis. Strictness analysis is straightforward in the simplest case, that of analysing a first-order functional language using just two strictness values, namely divergence and “don’t know”. Mycroft’s classical translation immediately yields perfectly valid Boolean constraint logic programs, which, when run, provide the desired strictness information. However, more sophisticated analysis requires more complex domains of strictness values. We recast Wadler’s classical analysis over a 2n-point domain as finite-domain constraint solving. This approach has several advantages. First, the translation is relatively simple. We translate a recursive function definition into one or two constraint program clauses, in a manner which naturally extends Mycroft’s translation for the 2-point case, where the classical approach translate the definition of an n-place function over lists into 4 n mutually recursive equations. Second, the resulting program produces relational information, allowing for example to ask which combinations of properties of input will produce a given output. Third, the approach allows us to leverage from established technology, for solving finite-domain constraints, as well as for finding fixed points. Finally, the use of (disjunctive) constraints can yield a higher precision in the analysis of some programs.