Computing and Information Systems - Research Publications

Permanent URI for this collection

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

Filters

2020 - 2023 4
Reset filters

Settings
Statistics
Citations
Author: Stuckey, Peter × Type: Chapter ×

Search Results

Now showing 1 - 4 of 4
  • Item
    No Preview Available
    Ballot-Polling Audits of Instant-Runoff Voting Elections with a Dirichlet-Tree Model
    Everest, F ; Blom, M ; Stark, PB ; Stuckey, PJ ; Teague, V ; Vukcevic, D (Springer International Publishing, 2023-01-01)
  • Item
    Thumbnail Image
    Lightweight Nontermination Inference with CHCs
    Kafle, B ; Gange, G ; Schachte, P ; Sondergaard, H ; Stuckey, PJ ; Calinescu, R ; Pasareanu, CS (SPRINGER INTERNATIONAL PUBLISHING AG, 2021)
    Non-termination is an unwanted program property (considered a bug) for some software systems, and a safety property for other systems. In either case, automated discovery of preconditions for non-termination is of interest. We introduce NtHorn, a fast lightweight non-termination analyser, able to deduce non-trivial sufficient conditions for non-termination. Using Constrained Horn Clauses (CHCs) as a vehicle, we show how established techniques for CHC program transformation and abstract interpretation can be exploited for the purpose of non-termination analysis. NtHorn is comparable in power to the state-of-the-art non-termination analysis tools, as measured on standard competition benchmark suites (consisting of integer manipulating programs), while typically solving problems an order of magnitude faster.
  • Item
    Thumbnail Image
    Disjunctive Interval Analysis
    Gange, G ; Navas, JA ; Schachte, P ; Sondergaard, H ; Stuckey, PJ ; Dragoi, C ; Mukherjee, S ; Namjoshi, K (SPRINGER INTERNATIONAL PUBLISHING AG, 2021)
    We revisit disjunctive interval analysis based on the Boxes abstract domain. We propose the use of what we call range decision diagrams (RDDs) to implement Boxes, and we provide algorithms for the necessary RDD operations. RDDs tend to be more compact than the linear decision diagrams (LDDs) that have traditionally been used for Boxes. Representing information more directly, RDDs also allow for the implementation of more accurate abstract operations. This comes at no cost in terms of analysis efficiency, whether LDDs utilise dynamic variable ordering or not. RDD and LDD implementations are available in the Crab analyzer, and our experiments confirm that RDDs are well suited for disjunctive interval analysis.
  • Item
    Thumbnail Image
    Abstract interpretation, symbolic execution and constraints
    Amadini, R ; Gange, G ; Schachte, P ; Sondergaard, H ; Stuckey, P ; de Boer, F ; Mauro, J (Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2020)
    Abstract interpretation is a static analysis framework for sound over-approximation of all possible runtime states of a program. Symbolic execution is a framework for reachability analysis which tries to explore all possible execution paths of a program. A shared feature between abstract interpretation and symbolic execution is that each – implicitly or explicitly – maintains constraints during execution, in the form of invariants or path conditions. We investigate the relations between the worlds of abstract interpretation, symbolic execution and constraint solving, to expose potential synergies.