Computing and Information Systems - Research Publications

Permanent URI for this collection

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

Filters

2015 - 2018 4
Reset filters

Settings
Statistics
Citations
Author: Schachte, Peter × Author: Stuckey, Peter × Type: Journal Article ×

Search Results

Now showing 1 - 4 of 4
  • 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
    Thumbnail Image
    Reference Abstract Domains and Applications to String Analysis
    Amadini, R ; Gange, G ; Gauthier, F ; Jordan, A ; Schachte, P ; Sondergaard, H ; Stuckey, PJ ; Zhang, C (IOS Press, 2018-02-09)
    Abstract interpretation is a well established theory that supports reasoning about the run-time behaviour of programs. It achieves tractable reasoning by considering abstractions of run-time states, rather than the states themselves. The chosen set of abstractions is referred to as the abstract domain. We develop a novel framework for combining (a possibly large number of) abstract domains. It achieves the effect of the so-called reduced product without requiring a quadratic number of functions to translate information among abstract domains. A central notion is a reference domain, a medium for information exchange. Our approach suggests a novel and simpler way to manage the integration of large numbers of abstract domains. We instantiate our framework in the context of string analysis. Browser-embedded dynamic programming languages such as JavaScript and PHP encourage the use of strings as a universal data type for both code and data values. The ensuing vulnerabilities have made string analysis a focus of much recent research. String analysis tends to combine many elementary string abstract domains, each designed to capture a specific aspect of strings. For this instance the set of regular languages, while too expensive to use directly for analysis, provides an attractive reference domain, enabling the efficient simulation of reduced products of multiple string abstract domains.
  • 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.