Computing and Information Systems - Research Publications

Permanent URI for this collection

http://hdl.handle.net/11343/350

Filters

2010 - 2016 5
Reset filters

Settings
Statistics
Citations
Author: Gange, Graeme × Author: Stuckey, Peter × End date: 2017 × Start date: 2010 × Type: Journal Article ×

Search Results

Now showing 1 - 5 of 5
  • Item
    Thumbnail Image
    Synthesizing Optimal Switching Lattices
    Gange, G ; Søndergaard, H ; Stuckey, PJ (Association for Computing Machinery, 2014-11)
    The use of nanoscale technologies to create electronic devices has revived interest in the use of regular structures for defining complex logic functions. One such structure is the switching lattice, a two-dimensional lattice of four-terminal switches. We show how to directly construct switching lattices of polynomial size from arbitrary logic functions; we also show how to synthesize minimal-sized lattices by translating the problem to the satisfiability problem for a restricted class of quantified Boolean formulas. The synthesis method is an anytime algorithm that uses modern SAT solving technology and dichotomic search. It improves considerably on an earlier proposal for creating switching lattices for arbitrary logic functions.
  • Item
    Thumbnail Image
    A complete refinement procedure for regular separability of context-free languages
    Gange, G ; Navas, JA ; Schachte, P ; Sondergaard, H ; Stuckey, PJ (ELSEVIER SCIENCE BV, 2016-04-25)
    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.
  • Item
    No Preview Available
    Horn Clauses As an Intermediate Representation for Program Analysis and Transformation
    Gange, G ; Navas Laserna, J ; Schachte, P ; SONDERGAARD, H ; Stuckey, PJ (Cambridge University Press, 2015)
    Abstract Many recent analyses for conventional imperative programs begin by transforming programs into logic programs, capitalising on existing LP analyses and simple LP semantics. We propose using logic programs as an intermediate program representation throughout the compilation process. With restrictions ensuring determinism and single-modedness, a logic program can easily be transformed to machine language or other low-level language, while maintaining the simple semantics that makes it suitable as a language for program analysis and transformation. We present a simple LP language that enforces determinism and single-modedness, and show that it makes a convenient program representation for analysis and transformation.
  • Item
    Thumbnail Image
    Interval Analysis and Machine Arithmetic: Why Signedness Ignorance Is Bliss
    Gange, G ; Navas, JA ; Schachte, P ; Sondergaard, H ; Stuckey, PJ (Association for Computing Machinery, 2015)
    The most commonly used integer types have fixed bit-width, making it possible for computations to “wrap around,” and many programs depend on this behaviour. Yet much work to date on program analysis and verification of integer computations treats integers as having infinite precision, and most analyses that do respect fixed width lose precision when overflow is possible. We present a novel integer interval abstract domain that correctly handles wrap-around. The analysis is signedness agnostic. By treating integers as strings of bits, only considering signedness for operations that treat them differently, we produce precise, correct results at a modest cost in execution time.
  • Item
    Thumbnail Image
    Fast Set Bounds Propagation Using a BDD-SAT Hybrid
    Gange, G ; Stuckey, PJ ; Lagoon, V (AI ACCESS FOUNDATION, 2010)
    Binary Decision Diagram (BDD) based set bounds propagation is a powerful approach to solving set-constraint satisfaction problems. However, prior BDD based techniques in- cur the significant overhead of constructing and manipulating graphs during search. We present a set-constraint solver which combines BDD-based set-bounds propagators with the learning abilities of a modern SAT solver. Together with a number of improvements beyond the basic algorithm, this solver is highly competitive with existing propagation based set constraint solvers.