Harald Sondergaard

String constraint solving: past, present and future

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

Conference Proceedings  |  2020  |  Frontiers in Artificial Intelligence and Applications

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

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  |  Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

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

Constraint Programming for Dynamic Symbolic Execution of JavaScript

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

Conference Proceedings  |  2019  |  16th International Conference, CPAIOR 2019, Proceedings

Dynamic Symbolic Execution (DSE) combines concrete and symbolic execution, usually for the purpose of generating good test suites ..

An iterative approach to precondition inference using constrained Horn clauses

Bishoksan Kafle, John P Gallagher, Graeme Gange, Peter Schachte, Harald Sondergaard, Peter J Stuckey

Journal article  |  2018  |  Theory and Practice of Logic Programming

Reference Abstract Domains and Applications to String Analysis

Roberto Amadini, Graeme Gange, Francois Gauthier, Alexander Jordan, Peter Schachte, Harald Sondergaard, Peter J Stuckey, Chenyi Zhang

Journal article  |  2018  |  Fundamenta Informaticae

Abstract interpretation is a well established theory that supports reasoning about the run-time behaviour of programs. It achieves..

Symbolic execution with invariant inlay: Evaluating the potential

Eman Alatawi, Timothy Miller, H Sondergaard

Conference Proceedings  |  2018  |  25th Australasian Software Engineering Conference (ASWEC)

Dynamic symbolic execution (DSE) is a non-standard execution mechanism which, loosely, executes a program symbolically and, simult..

Making sense of a learning management system's quiz analytics in understanding students' learning difficulties

A Mendoza, H Sondergaard, A Venables

Conference Proceedings  |  2017