Professor Harald Sondergaard

  • Room: Level: 08 Room: 8.16
  • Building: Doug McDonell Building
  • Campus: Parkville

Research interests

  • Boolean functions (Data structures and algorithms for Boolean functions)
  • Fixed point theory (Lattices; Order; Algorithms)
  • Program transformation (Compilation; Partial evaluation)
  • Programming languages (Programming language semantics; Declarative programming)
  • Software verification
  • Static analysis of software (Abstract interpretation)

Personal webpage


Harald Søndergaard is a Professor in the School of Computing and Information Systems at the University of Melbourne. His primary research areas are software reliability and security, program analysis, software verification, and declarative programming languages.

Harald received an MSc in Computer Science in 1987 and a PhD in 1989, both from the University of Copenhagen. He has been a member of academic staff at the University of Melbourne since 1990, serving as Deputy Head of Department in 2002-2003, as Associate Dean (Learning) in the Engineering Faculty from November 2001 to June 2006, and as Assistant Dean (Teaching Quality) in the Melbourne School of Engineering from July 2007 to June 2009. 

Harald has received national awards for teaching excellence (the inaugural CORE Teaching Award 2007 and a citation from the Australian Learning and Teaching Council in the same year) in addition to many local university awards.  He has been a member of the University's Teaching and Learning Development Committee for more than a decade and he publishes regularly on engineering and computer science education.

Recent publications

  1. Amadini R, Nazecic-Andrlon M, Gange G, Schachte P, Sondergaard H, Stuckey PJ. Constraint Programming for Dynamic Symbolic Execution of JavaScript. 16th International Conference, CPAIOR 2019, Thessaloniki, Greece, June 4–7, 2019, Proceedings. Springer Verlag. 2019, Vol. 11494 LNCS. DOI: 10.1007/978-3-030-19212-9_1
  2. Andrlon M, Schachte P, Sondergaard H, Stuckey PJ. Optimal Bounds for Floating-Point Addition in Constant Time. 2019 IEEE 26th Symposium on Computer Arithmetic (ARITH). IEEE. 2019. DOI: 10.1109/arith.2019.00038
  3. Wang W, Sondergaard H, Stuckey P. Wombit: A Portfolio Bit-Vector Solver Using Word-Level Propagation. Journal of Automated Reasoning. 2019, Vol. 63, Issue 3. DOI: 10.1007/s10817-018-9493-1
  4. Kafle B, Gallagher JP, Gange G, Schachte P, Sondergaard H, Stuckey P. An iterative approach to precondition inference using constrained Horn clauses. 34th International Conference on Logic Programming (ICLP). Cambridge University Press. 2018, Vol. 18, Issue 3-4. DOI: 10.1017/S1471068418000091
  5. Amadini R, Gange G, Gauthier F, Jordan A, Schachte P, Sondergaard H, Stuckey P, Zhang C. Reference Abstract Domains and Applications to String Analysis. FUNDAMENTA INFORMATICAE. IOS Press. 2018, Vol. 158, Issue 4. DOI: 10.3233/FI-2018-1650
  6. Alatawi E, Miller T, Sondergaard H. Symbolic Execution with Invariant Inlay: Evaluating the Potential. 2018 25TH AUSTRALASIAN SOFTWARE ENGINEERING CONFERENCE (ASWEC). IEEE. 2018. DOI: 10.1109/ASWEC.2018.00012
  7. Kafle B, Gange G, Schachte P, Sondergaard H, Stuckey P. A benders decomposition approach to deciding modular linear integer arithmetic. SAT 2017, the 20th International Conference on Theory and Applications of Satisfiability Testing. Springer Verlag. 2017, Vol. 10491 LNCS. DOI: 10.1007/978-3-319-66263-3_24
  8. Amadini R, Jordan A, Gange G, Gauthier F, Schachte P, Sondergaard H, Stuckey P, Zhang C. Combining String Abstract Domains for JavaScript Analysis: An Evaluation. 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) Held as Part of the 19th European Joint Conferences on Theory and Practice of Software (ETAPS). Springer Verlag. 2017, Vol. 10205. Editors: Legay A, Margaria T. DOI: 10.1007/978-3-662-54577-5_3
  9. Alatawi E, Sondergaard H, Miller T. Leveraging abstract interpretation for efficient dynamic symbolic execution. 32nd IEEE/ACM International Conference on Automated Software Engineering. IEEE Press. 2017. Editors: Rosu G, Di Penta M, Nguyen TN.
  10. Mendoza A, Sondergaard H, Venables A. Making sense of a learning management system's quiz analytics in understanding students' learning difficulties. 28th Annual Conference of the Australasian Association for Engineering Education. Australasian Association for Engineering Education. 2017. Editors: Huda N, Inglis D, Tse N, Town G.
  11. Wang W, Sondergaard H, Stuckey P. A bit-vector solver with word-level propagation. 13th International Conference on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming (CPAIOR). Springer International Publishing. 2016, Vol. LNCS 9676. Editors: Quimper C-G. DOI: 10.1007/978-3-319-33954-2_27
  12. Gange G, Navas JA, Schachte P, Sondergaard H, Stuckey P. A complete refinement procedure for regular separability of context-free languages. THEORETICAL COMPUTER SCIENCE. Elsevier Science. 2016, Vol. 625. DOI: 10.1016/j.tcs.2016.01.026
  13. Gange G, Navas Laserna J, Schachte P, Sondergaard H, Stuckey P. An abstract domain of uninterpreted functions. 17th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI). 2016, Vol. LNCS 9583. Editors: Jobstmann B, Leino KRM. DOI: 10.1007/978-3-662-49122-5
  14. Gange G, Navas JA, Schachte P, Sondergaard H, Stuckey PJ. An Abstract Domain of Uninterpreted Functions. Lecture Notes in Computer Science. Springer Verlag. 2016. DOI: 10.1007/978-3-662-49122-5_4
  15. Lin Y, Miller T, Sondergaard H. Compositional Symbolic Execution: Incremental Solving Revisited. 2016 23RD ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC 2016). IEEE. 2016. Editors: Potanin A, Murphy G. DOI: 10.1109/APSEC.2016.49

View a full list of publications on the University of Melbourne’s ‘Find An Expert’ profile