Arrow Research search

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

Possible papers

9

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

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 find 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