Author name cluster

Peter Schachte

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.

9 papers

2 author rows

LOPSTR Conference 2020 Conference Paper

Algorithm Selection for Dynamic Symbolic Execution: A Preliminary Study

Roberto Amadini
Graeme Gange
Peter Schachte
Harald Søndergaard
Peter J. Stuckey

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.

Details

ECAI Conference 2020 Conference Paper

String Constraint Solving: Past, Present and Future

Roberto Amadini
Graeme Gange
Peter Schachte
Harald Søndergaard
Peter J. Stuckey

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.

Details

IJCAI Conference 2018 Conference Paper

Machine Learning and Constraint Programming for Relational-To-Ontology Schema Mapping

Diego de Uña
Nataliia Rümmele
Graeme Gange
Peter Schachte
Peter J. Stuckey

The problem of integrating heterogeneous data sources into an ontology is highly relevant in the database field. Several techniques exist to approach the problem, but side constraints on the data cannot be easily implemented and thus the results may be inconsistent. In this paper we improve previous work by Taheriyan et al. [2016a] using Machine Learning (ML) to take into account inconsistencies in the data (unmatchable attributes) and encode the problem as a variation of the Steiner Tree, for which we use work by De Uña et al. [2016] in Constraint Programming (CP). Combining ML and CP achieves state-of-the-art precision, recall and speed, and provides a more flexible framework for variations of the problem.

PDF Details

SAT Conference 2017 Conference Paper

A Benders Decomposition Approach to Deciding Modular Linear Integer Arithmetic

Bishoksan Kafle
Graeme Gange
Peter Schachte
Harald Søndergaard
Peter J. Stuckey

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.

Details

TCS Journal 2016 Journal Article

A complete refinement procedure for regular separability of context-free languages

Graeme Gange
Jorge A. Navas
Peter Schachte
Harald Søndergaard
Peter J. Stuckey

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.

Details DOI

AAAI Conference 2016 Conference Paper

Steiner Tree Problems with Side Constraints Using Constraint Programming

Diego de Uña
Graeme Gange
Peter Schachte
Peter Stuckey

The Steiner Tree Problem is a well know NP-complete problem that is well studied and for which fast algorithms are already available. Nonetheless, in the real world the Steiner Tree Problem is almost always accompanied by side constraints which means these approaches cannot be applied. For many problems with side constraints, only approximation algorithms are known. We introduce here a propagator for the tree constraint with explanations, as well as lower bounding techniques and a novel constraint programming approach for the Steiner Tree Problem and two of its variants. We ﬁnd our propagators with explanations are highly advantageous when it comes to solving variants of this problem.

PDF Details

LOPSTR Conference 2014 Conference Paper

Analyzing Array Manipulating Programs by Program Transformation

J. Robert M. Cornish
Graeme Gange
Jorge A. Navas
Peter Schachte
Harald Søndergaard
Peter J. Stuckey

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.

Details

AIJ Journal 2010 Journal Article

Information loss in knowledge compilation: A comparison of Boolean envelopes

Peter Schachte
Harald Søndergaard
Leigh Whiting
Kevin Henshall

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.

Details DOI

TCS Journal 2003 Journal Article

Precise goal-independent abstract interpretation of constraint logic programs

Peter Schachte

We present a goal-independent abstract interpretation framework for constraint logic programs, and prove the sufficiency of a set of conditions for abstract domains to ensure that the analysis will never lose precision. Along the way, we formally define constraint logic programming systems, give a formal semantics that is independent of the actual constraint domain and the details of the proof algorithm, and formally define the maximally precise abstraction of a constraint logic program.

Details DOI