Harald Sondergaard

A Fresh Look at Zones and Octagons

Graeme Gange, Zequn Ma, Jorge A Navas, Peter Schachte, Harald Søndergaard, Peter J Stuckey

Journal article  |  2021  |  ACM Transactions on Programming Languages and Systems

Zones and Octagons are popular abstract domains for static program analysis. They enable the automated discovery of simple numeric..

Transformation-Enabled Precondition Inference

B Kafle, G Gange, PJ Stuckey, P Schachte, H SØndergaard

Journal article  |  2021  |  Theory and Practice of Logic Programming

Precondition inference is a non-trivial problem with important applications in program analysis and verification. We present a nov..

Disjunctive Interval Analysis

G Gange, JA Navas, P Schachte, H Søndergaard, PJ Stuckey

Book Chapter  |  2021  |  Lecture Notes in Artificial Intelligence

We revisit disjunctive interval analysis based on the Boxes abstract domain. We propose the use of what we call range decision dia..

Algorithm Selection for Dynamic Symbolic Execution: A Preliminary Study

R Amadini, G Gange, P Schachte, H Søndergaard, PJ Stuckey

Conference Proceedings  |  2021  |  Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Given a portfolio of algorithms, the goal of Algorithm Selection (AS) is to select the best algorithm(s) for a new, unseen problem..

Abstract interpretation, symbolic execution and constraints

R Amadini, G Gange, P Schachte, H Søndergaard, PJ Stuckey

Conference Proceedings  |  2020  |  OpenAccess Series in Informatics

String constraint solving: past, present and future

Roberto Amadini, Graeme Gange, Peter Schachte, Harald Sondergaard, Peter J Stuckey

Conference Proceedings  |  2020  |  24th European Conference on Artificial Intelligence, Proceedings

String constraint solving is an important emerging field, given the ubiquity of strings over different fields such as formal analy..

Abstract interpretation, symbolic execution and constraints

Roberto Amadini, Graeme Gange, Peter Schachte, Harald Sondergaard, Peter Stuckey

Book Chapter  |  2020

Abstract interpretation is a static analysis framework for sound over-approximation of all possible runtime states of a program. S..

Wombit: A Portfolio Bit-Vector Solver Using Word-Level Propagation

W Wang, H Søndergaard, PJ Stuckey

Journal article  |  2019  |  Journal of Automated Reasoning

We develop an idea originally proposed by Michel and Van Hentenryck of how to perform bit-vector constraint propagation on the wor..

Optimal Bounds for Floating-Point Addition in Constant Time

Mak Andrlon, Peter Schachte, Harald Sondergaard, Peter J Stuckey

Conference Proceedings  |  2019  |  Proceedings of the 2019 IEEE 26th Symposium on Computer Arithmetic (ARITH)

Reasoning about floating-point numbers is notoriously difficult, owing to the lack of convenient algebraic properties such as asso..

Dissecting widening: Separating termination from information

G Gange, JA Navas, P Schachte, H Søndergaard, PJ Stuckey

Conference Proceedings  |  2019  |  Programming Languages and Systems, 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1–4, 2019, Proceedings

Widening ensures or accelerates convergence of a program analysis, and sometimes contributes a guarantee of soundness that would o..