- Computing and Information Systems - Research Publications
Computing and Information Systems - Research Publications
Permanent URI for this collection
3 results
Filters
Reset filtersSettings
Statistics
Citations
Search Results
Now showing
1 - 3 of 3
-
ItemLightweight Nontermination Inference with CHCsKafle, 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.
-
ItemDisjunctive Interval AnalysisGange, 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.
-
ItemAbstract interpretation, symbolic execution and constraintsAmadini, 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.