Harald Søndergaard

Selected papers grouped in the following areas:

• Symbolic Execution and Partial Evaluation
• Termination Analysis
• String Analysis
• Program Analysis and Verification
• Constraint Solving
• Determining Fixed Points
• Planning and Scheduling
• Circuit Optimization
• Programming Language Concepts and Semantics
• Logic Programming Language Technologies
• Memory Management
• Boolean Approximation
• Abstract Interpretation of Logic Programs
• Analysis of Functional Programs
• Computer Science Education

Scholar citation profile

Symbolic Execution and Partial Evaluation:

• Peter Sestoft and Harald Søndergaard. The genesis of Mix: Early days of self-applicable partial evaluation (invited contribution). In G. Keller and M. Wang, Proceedings of the 2024 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation, pages 1-13. ACM Press, 2024.
  Bibtex DOI 10.1145/3635800.3637445
• Roberto Amadini, Graeme Gange, Peter Schachte, Harald Søndergaard and Peter J. Stuckey. Algorithm selection for dynamic symbolic execution: A preliminary study. In M. Fernández, editor, Logic-Based Program Synthesis and Transformation (LOPSTR'20) (Lecture Notes in Computer Science 12561), pages 192-209. Springer 2021.
  Bibtex DOI 10.1007/978-3-030-68446-4_10
• Roberto Amadini, Graeme Gange, Peter Schachte, Harald Søndergaard and Peter J. Stuckey. Abstract interpretation, symbolic execution and constraints. In F. S. de Boer and J. Mauro, editors, Recent Developments in the Design and Implementation of Programming Languages (OpenAccess Series in Informatics 86), pages 7:1-7:19. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2020.
  PDF Bibtex DOI 10.4230/OASIcs.Gabbrielli.2020.7
• Roberto Amadini, Mak Andrlon, Graeme Gange, Peter Schachte, Harald Søndergaard and Peter J. Stuckey. Constraint programming for dynamic symbolic execution of JavaScript. In L.-M. Rousseau and K. Stergiou, editors, Integration of Constraint Programming, Artificial Intelligence, and Operations Research: Proceedings of the 16th International Conference (CPAIOR 2019) (Lecture Notes in Computer Science 11494), pages 1-19. Springer 2019.
  PDF https://minerva-access.unimelb.edu.au/rest/bitstreams/b999c802-90f6-5ce4-8b79-c298bfc62afa/retrieve Bibtex DOI 10.1007/978-3-030-19212-9_1
• Eman Alatawi, Tim Miller and Harald Søndergaard. Symbolic execution with invariant inlay: Evaluating the potential. In Proceedings of the 25th Australasian Software Engineering Conference (ASWEC 2018), pages 26-30. IEEE Conference Publishing Services, 2018.
  PDF Bibtex DOI 10.1109/ASWEC.2018.00012
• Eman Alatawi, Harald Søndergaard and Tim Miller. Leveraging abstract interpretation for efficient dynamic symbolic execution. In G. Rosu, M. Di Penta and T. N. Nguyen, editors, Proceedings of the 32nd ACM/IEEE International Conference on Automated Software Engineering (ASE 2017), pages 619-624. IEEE Computer Society, 2017.
  PDF Bibtex DOI 10.1109/ASE.2017.8115672
• Yude Lin, Tim Miller and Harald Søndergaard. Compositional symbolic execution: Incremental solving revisited. In A. Potanin and G. Murphy, editors, APSEC'16: Proceedings of the 23rd Asia-Pacific Software Engineering Conference, pages 273-280. Hamilton, NZ, 2016.
  Bibtex DOI 10.1109/APSEC.2016.046
• Eman Alatawi, Tim Miller and Harald Søndergaard. Generating source inputs for metamorphic testing using dynamic symbolic execution. In Proceedings of the First International Workshop on Metamorphic Testing (MET 2016), pages 19-25. ACM, 2016.
  Bibtex DOI 10.1145/2896971.2896980
• Eman Alatawi, Tim Miller and Harald Søndergaard. Using metamorphic testing to improve dynamic symbolic execution. Proceedings of the 24th Australasian Software Engineering Conference (ASWEC 2015), pages 38-47. IEEE Conference Publishing Services, 2015.
  Bibtex DOI 10.1109/ASWEC.2015.16
• Yude Lin, Tim Miller and Harald Søndergaard. Compositional symbolic execution using fine-grained summaries. Proceedings of the 24th Australasian Software Engineering Conference (ASWEC 2015), pages 213-222. IEEE Conference Publishing Services, 2015.
  PDF Bibtex DOI 10.1109/ASWEC.2015.32
• Trevor Hansen, Peter Schachte and Harald Søndergaard. State joining and splitting for the symbolic execution of binaries. In S. Bensalem and D. A. Peled, editors, Runtime Verification (Lecture Notes in Computer Science 5779), pages 76-92, Springer, 2009.
  Bibtex DOI 10.1007/978-3-642-04694-0_6
• Peter Sestoft and Harald Søndergaard, editors. PEPM'94: Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, Orlando, Florida, June 1994. Technical Report 94/9, Dept. of Computer Science, The University of Melbourne, 1994.
  Bibtex
• Neil Jones, Peter Sestoft and Harald Søndergaard. Mix: A self-applicable partial evaluator for experiments in compiler generation. Lisp and Symbolic Computation 2 (1): 9-50, 1989.
  Bibtex DOI 10.1007/BF01806312
• Peter Sestoft and Harald Søndergaard. A bibliography on partial evaluation. SIGPLAN Notices 23 (2): 19-27, 1988.
  PDF Bibtex DOI 10.1145/43908.43910
• Neil Jones, Peter Sestoft and Harald Søndergaard. Mix: A self-applicable partial evaluator for experiments in compiler generation - extended abstract. In M. Main et al., editors, Mathematical Foundations of Programming Language Semantics (Lecture Notes in Computer Science 298), pages 386-413. Springer-Verlag, 1987.
  Bibtex DOI 10.1007/3-540-19020-1_21
• Neil Jones, Peter Sestoft and Harald Søndergaard. An experiment in partial evaluation: The generation of a compiler generator. In J.-P. Jouannaud, editor, Rewriting Techniques and Applications (Lecture Notes in Computer Science 202), pages 124-140. Springer-Verlag, 1985. (Reviewed in Computing Reviews 27 (7): 353, 1986.)
  Bibtex DOI 10.1007/3-540-15976-2_6

Termination Analysis:

• Bishoksan Kafle, Graeme Gange, Peter Schachte, Harald Søndergaard and Peter J. Stuckey. A lightweight approach to nontermination inference using Constrained Horn Clauses. Software and Systems Modeling, to appear.
• Bishoksan Kafle, Graeme Gange, Peter Schachte, Harald Søndergaard and Peter J. Stuckey. Lightweight non-termination inference with CHCs. In R. Calinescu and C. S. Păsăreanu, editors, Software Engineering and Formal Methods, (Lecture Notes in Computer Science 13085), pages 383-402. Springer, 2021.
  PDF Bibtex DOI 10.1007/978-3-030-92124-8_22
• Chris Speirs, Zoltan Somogyi and Harald Søndergaard. Termination analysis for Mercury. In P. Van Hentenryck, editor, Static Analysis: Proceedings of the Fourth International Symposium (Lecture Notes in Computer Science 1302), pages 157-171. Springer, 1997.
  Bibtex DOI 10.1007/bfb0032740
• James Bailey, Lobel Crnogorac, Kotagiri Ramamohanarao and Harald Søndergaard. Abstract interpretation of active rules and its use in termination analysis. In F. Afrati and P. Kolaitis, editors, Database Theory (ICDT'97) (Lecture Notes in Computer Science 1186), pages 188-202. Springer, 1997.
  Bibtex DOI 10.1007/3-540-62222-5_45

String Analysis:

• H. Søndergaard. String abstract domains and their combination. In E. De Angelis and W. Vanhoof, editors, Logic-Based Program Synthesis and Transformation (Lecture Notes in Computer Science 13290), pages 1-15. Springer, 2022.
  PDF Bibtex DOI 10.1007/978-3-030-98869-2_1
• R. Amadini, G. Gange, F. Gauthier, A. Jordan, P. Schachte, H. Søndergaard, P. J. Stuckey and C. Zhang. Reference abstract domains and applications to string analysis. Fundamenta Informaticae 158(4): 297-326, 2018.
  PDF Bibtex DOI 10.3233/FI-2018-1650
• R. Amadini, A. Jordan, G. Gange, F. Gauthier, P. Schachte, H. Søndergaard, P. J. Stuckey and C. Zhang. Combining string abstract domains for JavaScript analysis: An evaluation. In A. Legay and T. Margaria, editors, Tools and Algorithms for the Construction and Analysis of Systems: Proceedings of the 23rd International Conference (TACAS 2017) (Lecture Notes in Computer Science 10205), pages 41-57. Springer, 2017.
  Bibtex DOI 10.1007/978-3-662-54577-5_3
• Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard and Peter J. Stuckey. A complete refinement procedure for regular separability of context-free languages. Theoretical Computer Science 625: 1-24, 2016.
  Bibtex DOI 10.1016/j.tcs.2016.01.026
• Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard and Peter J. Stuckey. A tool for intersecting context-free grammars and its applications. In K. Havelund, G. Holzmann and R. Joshi, editors, NASA Formal Methods: Proceedings of the Seventh International Symposium (Lecture Notes in Computer Science 9058), pages 422-428. Springer, 2015.
  Bibtex DOI 10.1007/978-3-319-17524-9

Program Analysis and Verification:

• Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard and Peter J. Stuckey. Disjunctive interval analysis. In C. Drăgoi, S. Mukherjee and K. Namjoshi, editors, Static Analysis (Lecture Notes in Computer Science 12913), pages 144-165. Springer, 2021.
  PDF Bibtex DOI 10.1007/978-3-030-88806-0_7
• Bishoksan Kafle, Graeme Gange, Peter J. Stuckey, Peter Schachte and Harald Søndergaard. Transformation-enabled precondition inference. Theory and Practice of Logic Programming, 21(6): 700-716, 2021.
  PDF Bibtex DOI 10.1017/S1471068421000272
• Graeme Gange, Zequn Ma, Jorge A. Navas, Peter Schachte, Harald Søndergaard and Peter J. Stuckey. A fresh look at Zones and Octagons. ACM Transactions on Programming Languages and Systems 43(3): 11:1-11:51, 2021.
  PDF Bibtex DOI 10.1145/3457885
• Bishoksan Kafle, John Gallagher, Graeme Gange, Peter Schachte, Harald Søndergaard and Peter J. Stuckey. An iterative approach to precondition inference using constrained Horn clauses. Theory and Practice of Logic Programming 18(3-4): 553-570, 2018.
  Bibtex DOI 10.1017/S1471068418000091
• Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard and Peter J. Stuckey. Exploiting sparsity in difference-bound matrices. In X. Rival, editor, Static Analysis (Lecture Notes in Computer Science 9837), pages 189-211. Springer International Publishing, 2016.
  Bibtex DOI 10.1007/978-3-662-53413-7
• Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard and Peter J. Stuckey. An abstract domain of uninterpreted functions. In B. Jobstmann and K. R. M. Leino, editors, Verification, Model Checking and Abstract Interpretation (Lecture Notes in Computer Science 9583), pages 85-103. Springer International Publishing, 2016.
  Bibtex DOI 10.1007/978-3-662-49122-5
• Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard and Peter J. Stuckey. Horn clauses as an intermediate representation for program analysis and transformation. Theory and Practice of Logic Programming 15(4-5): 526-542, 2015.
  Bibtex DOI 10.1017/S1471068415000204
• Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard and Peter J. Stuckey. Interval analysis and machine arithmetic: Why signedness ignorance is bliss. ACM Transactions on Programming Languages and Systems 37(1): 1:1-1:35, 2015.
  Bibtex DOI 10.1145/2651360
• J. Robert M. Cornish, Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard and Peter J. Stuckey. Analyzing array manipulating programs by program transformation. In M. Proietti and H. Seki, editors, Logic-Based Program Synthesis and Transformation (LOPSTR'14) (Lecture Notes in Computer Science 8981), pages 3-20. Springer, 2015.
  Bibtex DOI 10.1007/978-3-319-17822-6_1
• Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard and Peter J. Stuckey. Abstract interpretation over non-lattice abstract domains. In F. Logozzo and M. Fähndrich, editors, Static Analysis (Lecture Notes in Computer Science 7935), pages 6-24. Springer, 2013.
  PDF Bibtex DOI 10.1007/978-3-642-38856-9_3
• Jorge A. Navas, Peter Schachte, Harald Søndergaard and Peter J. Stuckey. Signedness-agnostic program analysis: Precise integer bounds for low-level code. In R. Jhala and A. Igarashi, editors, APLAS 2012: Proceedings of the 10th Asian Symposium on Programming Languages and Systems (Lecture Notes in Computer Science 7705), pages 115-130. Springer, 2012.
  Bibtex DOI 10.1007/978-3-642-35182-2_9
• Andy King and Harald Søndergaard. Automatic abstraction for congruences. In G. Barthe and M. Hermenegildo, editors, Verification, Model Checking and Abstract Interpretation (Lecture Notes in Computer Science 5944), pages 197-213. Springer, 2010.
  Bibtex DOI 10.1007/978-3-642-11319-2_16
• Andy King and Harald Søndergaard. Inferring congruence equations with SAT. In A. Gupta and S. Malik, editors, Proceedings of the 20th International Conference on Computer Aided Verification (Lecture Notes in Computer Science 5123), pages 281-293. Springer, 2008.
  Bibtex DOI 10.1007/978-3-540-70545-1_26

Constraint Solving:

• Roberto Amadini, Graeme Gange, Peter Schachte, Harald Søndergaard and Peter J. Stuckey. String constraint solving: Past, present and future. In G. De Giacomo et al., editors, Proceedings of the 24th European Conference on Artificial Intelligence, pages 2875-2876. IOS Press, 2020.
  PDF Bibtex DOI 10.3233/FAIA200431
• Mak Andrlon, Peter Schachte, Harald Søndergaard and Peter J. Stuckey. Optimal bounds for floating-point addition in constant time. In N. Takagi, S. Boldo and M. Langhammer, editors, Proceedings of the 26th IEEE Symposium on Computer Arithmetic (ARITH 2019), pages 159-166. IEEE Conf. Publ., 2019.
  PDF Bibtex DOI 10.1109/arith.2019.00038
• Wenxi Wang, Harald Søndergaard and Peter J. Stuckey. Wombit: A portfolio bit-vector solver using word-level propagation. Journal of Automated Reasoning 63(3): 723-762, 2019.
  PDF Bibtex DOI 10.1007/s10817-018-9493-1
• Bishoksan Kafle, Graeme Gange, Peter Schachte, Harald Søndergaard and Peter J. Stuckey. A Benders decomposition approach to deciding modular linear integer arithmetic. In S. Gaspers and T. Walsh, editors, Theory and Applications of Satisfiability Testing - SAT 2017 (Lecture Notes in Computer Science 10491), pages 380-397. Springer, 2017.
  Bibtex DOI 10.1007/978-3-319-66263-3_24
• Wenxi Wang, Harald Søndergaard and Peter J. Stuckey. A bit-vector solver with word-level propagation. In C.-G. Quimper, editor, Integration of AI and OR Techniques in Constraint Programming: Proceedings of the 13th International Conference (Lecture Notes in Computer Science 9676), pages 374-391. Springer International Publishing, 2016.
  Bibtex DOI 10.1007/978-3-319-33954-2_27
• Graeme Gange, Harald Søndergaard, Peter J. Stuckey and Peter Schachte. Solving difference constraints over modular arithmetic. In M. P. Bonacina, editor, Proceedings of the 24th International Conference on Automated Deduction (Lecture Notes in Artificial Intelligence 7898), pages 215-230. Springer, 2013.
  Bibtex DOI 10.1007/978-3-642-38574-2_15
• Graeme Gange, Jorge A. Navas, Peter J. Stuckey, Harald Søndergaard and Peter Schachte. Unbounded model-checking with interpolation for regular language constraints. In N. Piterman and S. Smolka, editors, TACAS 2013: Tools and Algorithms for the Construction and Analysis of Systems (Lecture Notes in Computer Science 7795), pages 277-291. Springer, 2013.
  Bibtex DOI 10.1007/978-3-642-36742-7_20

Determining Fixed Points:

• Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard and Peter J. Stuckey. Dissecting widening: Separating termination from information. In A. W. Lin, editor, Proceedings of the 17th Asian Symposium on Programming Languages and Systems (Lecture Notes in Computer Science 11893), pages 95-114. Springer, 2019.
  PDF Bibtex DOI 10.1007/978-3-030-34175-6_6
• Brian Herlihy, Peter Schachte and Harald Søndergaard. Un-Kleene Boolean equation solving. International Journal of Foundations of Computer Science 18 (2): 227-250, 2007.
  PDF Bibtex DOI 10.1142/S0129054107004668
• Brian Herlihy, Peter Schachte and Harald Søndergaard. Boolean equation solving as graph traversal. In J. Gudmundsson and B. Jay, editors, Theory of Computing 2006, Hobart, Australia, 2006. Conferences in Research and Practice in Information Technology 51, pages 123-132. Australian Computer Society, 2006.
  PDF Bibtex
• Kevin Glynn and Harald Søndergaard. Immediate fixpoints for strictness analysis. In J. Edwards, editor, Proceedings of the 22nd Australasian Computer Science Conference, Australian Computer Science Communications 21 (1): 336-347. Springer, 1999.
  Bibtex
• Harald Søndergaard. Immediate fixpoints and their use in groundness analysis. In V. Chandru and V. Vinay, editors, Foundations of Software Technology and Theoretical Computer Science (Lecture Notes in Computer Science 1180), pages 359-370. Springer, 1996.
  Bibtex DOI 10.1007/3-540-62034-6_63

Planning and Scheduling

• Toby Davies, Adrian Pearce, Peter Stuckey and Harald Søndergaard. Optimisation and relaxation for multiagent planning in the situation calculus. In R. H. Bordini, E. Elkind, G. Weiss and P. Yolum, editors, Proceedings of the 14th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2015), pages 1141-1149. IFAAMAS, 2015.
  PDF Bibtex
• Toby Davies, Adrian Pearce, Peter Stuckey and Harald Søndergaard. Fragment-based planning using column generation. In S. Chien, M. Do, A. Fern and W. Ruml, editors, Proceedings of the 24th International Conference on Automated Planning and Scheduling (ICAPS'14), pages 83-91. AAAI Publ., 2014.
  PDF Bibtex DOI 10.1609/icaps.v24i1.13628

Circuit Optimization

• Graeme Gange, Harald Søndergaard and Peter J. Stuckey. Synthesizing optimal switching lattices. ACM Transactions on Design Automation of Electronic Systems 20 (1): 6:1-6:14, 2014.
  PDF Bibtex DOI 10.1145/2661632
• Graeme Gange, Benjamin Horsfall, Lee Naish and Harald Søndergaard. Four-valued reasoning and cyclic circuits. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 33 (7): 1003-1016, 2014.
  Bibtex DOI 10.1109/TCAD.2014.2304176

Programming Language Concepts and Semantics:

• Lee Naish and Harald Søndergaard. Truth versus information in logic programming. Theory and Practice of Logic Programming 14 (6): 803-840, 2014.
  Bibtex DOI 10.1017/S1471068413000069
• Lee Naish, Harald Søndergaard and Benjamin Horsfall. Logic programming: From underspecification to undefinedness. In J. Mestre, editor, Computing: The Australasian Theory Symposium (CATS 2012), Melbourne, Australia, 2012. Conferences in Research and Practice in Information Technology 128, pages 49-58. Australian Computer Society, 2012.
  PDF Bibtex
• Harald Søndergaard and Peter Sestoft. Non-determinism in functional languages. The Computer Journal 35 (5): 514-523, 1992.
  Bibtex DOI 10.1093/comjnl/35.5.514
• Harald Søndergaard and Peter Sestoft. Referential transparency, definiteness and unfoldability. Acta Informatica 27 (6): 505-517, 1990. (Reviewed in Computing Reviews 32 (3): 144-145, 1991.)
  Bibtex DOI 10.1007/BF00277387

Logic Programming Language Technologies:

• Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard and Peter J. Stuckey. Failure tabled constraint logic programming by interpolation. Theory and Practice of Logic Programming 13 (4-5): 593-607, 2013.
  Bibtex DOI 10.1017/S1471068413000379
• Andrew Kelly, Kim Marriott, Harald Søndergaard and Peter J. Stuckey. A practical object-oriented analysis engine for constraint logic programs. Software - Practice and Experience 28 (2): 199-224, 1998.
  Bibtex DOI 10.1002/(SICI)1097-024X(199802)28:2<199::AID-SPE150>3.0.CO;2-4
• Andrew Kelly, Kim Marriott, Harald Søndergaard and Peter J. Stuckey. A generic object-oriented incremental analyser for constraint logic programs. In R. Kotagiri and J. Zobel, editors, Proceedings of the Twentieth Australasian Computer Science Conference, Australian Computer Science Comm. 19 (1): 92-101, 1997.
  PDF Bibtex
• Lobel Crnogorac, Andrew Kelly and Harald Søndergaard. A comparison of three occur-check analysers. In R. Cousot and D. A. Schmidt, editors, Static Analysis: Proceedings of the Third International Symposium (Lecture Notes in Computer Science 1145), pages 159-173. Springer, 1996.
  Bibtex DOI 10.1007/3-540-61739-6_40
• Andrew Kelly, Kim Marriott, Harald Søndergaard and Peter J. Stuckey. Two applications of an incremental analysis engine for (constraint) logic programs (system description). In R. Cousot and D. A. Schmidt, editors, Static Analysis: Proceedings of the Third International Symposium (Lecture Notes in Computer Science 1145), pages 385-386. Springer, 1996.
  Bibtex DOI 10.1007/3-540-61739-6_55
• Andrew Kelly, Andrew Macdonald, Kim Marriott, Harald Søndergaard, Peter J. Stuckey and Roland Yap. An optimizing compiler for CLP(R). In U. Montanari and F. Rossi, editors, Principles and Practice of Constraint Programming - CP'95 (Lecture Notes in Computer Science 976), pages 222-239. Springer, 1995.
  Bibtex DOI 10.1007/3-540-60299-2_14
• Kim Marriott, Harald Søndergaard, Peter J. Stuckey and Roland Yap. Optimizing compilation for CLP(R). In G. Gupta, editor, Proceedings of the 17th Australian Computer Science Conference, Australian Computer Science Communications 16 (1): 551-560, 1994.
  PDF Bibtex
• Kim Marriott and Harald Søndergaard. Difference-list transformation for Prolog. New Generation Computing 11 (2): 125-157, 1993.
  Bibtex DOI 10.1007/BF03037156
• Kim Marriott and Harald Søndergaard. On Prolog and the occur check problem. SIGPLAN Notices 24 (5): 76-82, 1989.
  PDF Bibtex DOI 10.1145/43908.43910

Memory Management:

• Matthew Davis, Peter Schachte, Zoltan Somogyi and Harald Søndergaard. A low overhead method for recovering unused memory inside regions. MSPC 2013: Proceedings of the ACM Workshop on Memory Systems Performance and Correctness, to appear. ACM Press, 2013.
  Bibtex DOI 10.1145/2492408.2492415
• Matthew Davis, Peter Schachte, Zoltan Somogyi and Harald Søndergaard. Towards region based memory management for Go. MSPC 2012: Proceedings of the ACM Workshop on Memory Systems Performance and Correctness, pages 58-67. ACM Press, 2012.
  Bibtex DOI 10.1145/2247684.2247695

Boolean Approximation:

• Kevin Henshall, Peter Schachte, Harald Søndergaard and Leigh Whiting. An algorithm for affine approximation of binary decision diagrams. Chicago Journal of Theoretical Computer Science 2010 (8), 2010.
  PDF Bibtex DOI 10.4086/cjtcs.2010.011
• Peter Schachte, Harald Søndergaard, Leigh Whiting and Kevin Henshall. Information loss in knowledge compilation: A comparison of Boolean envelopes. Artificial Intelligence 174 (9-10): 585-596, 2010.
  Bibtex DOI 10.1016/j.artint.2010.03.003
• Kevin Henshall, Peter Schachte, Harald Søndergaard and Leigh Whiting. Boolean affine approximation with binary decision diagrams. In R. Downey and P. Manyem, editors, Computing: The Australasian Theory Symposium (CATS 2009), Wellington, New Zealand, 2009. Conferences in Research and Practice in Information Technology 94, pages 121-129. Australian Computer Society, 2009.
  PDF Bibtex
• Peter Schachte and Harald Søndergaard. Boolean approximation revisited. In I. Miguel and W. Ruml, editors, Abstraction, Reformulation and Approximation (Lecture Notes in Artificial Intelligence 4612), pages 329-343. Springer, 2007.
  Bibtex DOI 10.1007/978-3-540-73580-9_26
• Peter Schachte and Harald Søndergaard. Closure operators for ROBDDs. In E. A. Emerson and K. S. Namjoshi, editors, Proceedings of the Seventh International Conference on Verification, Model Checking and Abstract Interpretation (Lecture Notes in Computer Science 3855), pages 1-16. Springer, 2006.
  Bibtex DOI 10.1007/11609773_1

Abstract Interpretation of Logic Programs:

• Michael Codish and Harald Søndergaard. Meta-circular abstract interpretation in Prolog. In T. Mogensen, D. Schmidt and I. H. Sudborough, editors, The Essence of Computation: Complexity, Analysis, Transformation (Lecture Notes in Computer Science 2566), pages 109-134. Springer, 2002.
  Bibtex DOI 10.1007/3-540-36377-7_6
• Michael Codish, Samir Genaim, Harald Søndergaard and Peter J. Stuckey. Higher-precision groundness analysis. In P. Codognet, editor, Logic Programming: Proceedings of the 17th International Conference (Lecture Notes in Computer Science 2237), pages 135-149. Springer, 2001.
  Bibtex DOI 10.1007/3-540-45635-x_17
• Michael Codish, Harald Søndergaard and Peter J. Stuckey. Sharing and groundness dependencies in logic programs. ACM Transactions on Programming Languages and Systems 21 (5): 948-976, 1999.
  Bibtex DOI 10.1145/330249.330252
• Michael Codish and Harald Søndergaard. The Boolean logic of set sharing analysis. In C. Palamidessi, H. Glaser and K. Meinke, editors, Principles of Declarative Programming: Proceedings of the Tenth International Symposium (Lecture Notes in Computer Science 1490), pages 89-101. Springer, 1998.
  PDF Bibtex DOI 10.1007/bfb0056609
• Maria Garcia de la Banda, Kim Marriott, Peter J. Stuckey and Harald Søndergaard. Differential methods in logic program analysis. Journal of Logic Programming 35 (1): 1-37, 1998.
  Bibtex DOI 10.1016/s0743-1066(97)10002-4
• Tania Armstrong, Kim Marriott, Peter Schachte and Harald Søndergaard. Two classes of Boolean functions for dependency analysis. Science of Computer Programming 31 (1): 3-45, 1998.
  Bibtex DOI 10.1016/S0167-6423(96)00039-1
• Harald Søndergaard. Immediate fixpoints and their use in groundness analysis. In V. Chandru and V. Vinay, editors, Foundations of Software Technology and Theoretical Computer Science (Lecture Notes in Computer Science 1180), pages 359-370. Springer, 1996.
  Bibtex DOI 10.1007/3-540-62034-6_63
• Tania Armstrong, Kim Marriott, Peter Schachte and Harald Søndergaard. Boolean functions for dependency analysis: Algebraic properties and efficient representation. In B. Le Charlier, editor, Static Analysis: Proceedings of the First International Symposium (Lecture Notes in Computer Science 864), pages 266-280. Springer-Verlag, 1994.
  PDF (technical report) Bibtex DOI 10.1007/3-540-58485-4_46
• Kim Marriott, Harald Søndergaard and Neil Jones. Denotational abstract interpretation of Prolog. ACM Transactions on Programming Languages and Systems 16 (3): 607-648, 1994.
  PDF Bibtex DOI 10.1145/177492.177650
• Kim Marriott and Harald Søndergaard. On propagation-based analysis of logic programs. In S. Michaylov and W. Winsborough, editors, Proceedings of the ILPS 93 Post-Conference Workshop on Global Compilation, pages 47-65. Vancouver, Canada, 1993.
  PDF Bibtex
• Kim Marriott and Harald Søndergaard. Precise and efficient groundness analysis for logic programs. ACM Letters on Programming Languages and Systems 2 (1-4): 181-196, 1993.
  PDF Bibtex DOI 10.1145/176454.176519
• Naomi Baker and Harald Søndergaard. Definiteness analysis for CLP(R). In G. Gupta, G. Mohay and R. Topor, editors, Proceedings of the 16th Australian Computer Science Conference, Australian Computer Science Communications 15 (1): 321-332, 1993.
  PDF Bibtex
• Kim Marriott and Harald Søndergaard. Bottom-up dataflow analysis of normal logic programs. Journal of Logic Programming 13 (2 & 3): 181-204, 1992.
  Bibtex DOI 10.1016/0743-1066(92)90031-W
• Roberto Cremonini, Kim Marriott and Harald Søndergaard. A general theory for abstraction. In C. P. Tsang, editor, AI '90: Proceedings of the Fourth Australian Joint Conference on Artificial Intelligence, pages 121-134. World Scientific Publ., 1990.
  PDF Bibtex
• Kim Marriott and Harald Søndergaard. Analysis of constraint logic programs. In S. Debray and M. Hermenegildo, editors, Logic Programming: Proceedings of the 1990 North American Conference, pages 531-547. MIT Press, 1990.
  PDF Bibtex
• Kim Marriott, Harald Søndergaard and Philip Dart. A characterization of non-floundering logic programs. In S. Debray and M. Hermenegildo, editors, Logic Programming: Proceedings of the 1990 North American Conference, pages 661-680. MIT Press, 1990.
  PDF Bibtex
• Kim Marriott and Harald Søndergaard. Abstract interpretation of logic programs: The denotational approach. In A. Bossi, editor, Proceedings of the Fifth Italian Conference on Logic Programming, pages 399-425. Gruppo Ricercatori ed Utenti di Logic Programming, Padova, Italy, 1990.
  PDF Bibtex
• Harald Søndergaard. Semantics-Based Analysis and Transformation of Logic Programs. PhD Thesis, University of Copenhagen, Denmark, 1989.
  PDF Bibtex
• Kim Marriott and Harald Søndergaard. Semantics-based dataflow analysis of logic programs. In G. X. Ritter, editor, Information Processing 89, pages 601-606. North-Holland, 1989.
  PDF Bibtex
• Kim Marriott and Harald Søndergaard. A tutorial on abstract interpretation of logic programs. Tutorial notes for the 1989 North American Conference on Logic Programming.
  PDF Bibtex
• Kim Marriott and Harald Søndergaard. On describing success patterns of logic programs. Technical Report 88/12. Department of Computer Science, The University of Melbourne, 1988.
  PDF Bibtex
• Kim Marriott and Harald Søndergaard. Bottom-up abstract interpretation of logic programs. In R. A. Kowalski and K. A Bowen, editors, Logic Programming: Proceedings of the Fifth International Conference and Symposium, pages 733-748. MIT Press, 1988.
  Bibtex
• Neil Jones and Harald Søndergaard. A semantics-based framework for the abstract interpretation of Prolog. In S. Abramsky and C. Hankin, editors, Abstract Interpretation of Declarative Languages, Chapter 6, pages 123-142. Ellis Horwood, 1987.
  PDF Bibtex
• Harald Søndergaard. An application of abstract interpretation of logic programs: Occur check reduction. In B. Robinet and R. Wilhelm, editors, Proceedings of the European Symposium on Programming 86 (Lecture Notes in Computer Science 213), pages 327-338. Springer-Verlag, 1986.
  PDF Bibtex DOI 10.1007/3-540-16442-1_25

Analysis of Functional Programs:

• Kevin Glynn, Peter J. Stuckey, Martin Sulzmann and Harald Søndergaard. Exception analysis for non-strict languages. Proceedings of the 2002 ACM SIGPLAN International Conference on Functional Programming, pages 98-109. ACM Press, 2002.
  Bibtex DOI 10.1145/581478.581488
• Kevin Glynn, Peter J. Stuckey, Martin Sulzmann and Harald Søndergaard. Boolean constraints for binding-time analysis. In O. Danvy and A. Filinsky, editors, Programs as Data Objects: Proceedings of the Second Symposium (Lecture Notes in Computer Science 2053), pages 39-63. Springer, 2001.
  Bibtex DOI 10.1007/3-540-44978-7_4
• Tihomir Gabric, Kevin Glynn and Harald Søndergaard. Strictness analysis as finite-domain constraint solving. In P. Flener, editor, Logic-Based Program Synthesis and Transformation (Lecture Notes in Computer Science 1559), pages 255-270. Springer, 1999.
  Bibtex DOI 10.1007/3-540-48958-4_14
• Kevin Glynn and Harald Søndergaard. Immediate fixpoints for strictness analysis. In J. Edwards, editor, Proceedings of the 22nd Australasian Computer Science Conference, Australian Computer Science Communications 21 (1): 336-347. Springer, 1999.
  Bibtex

Computer Science Education:

• Matthew Farrugia-Roberts, Bryn Jeffries and Harald Søndergaard. Teaching simple constructive proofs with Haskell programs. In P. Achten and E. Machkasova, editors, Trends in Functional Programming in Education (TFPIE) (Electronic Proceedings in Theoretical Computer Science 363), pages 54-75, 2022.
  PDF Bibtex DOI 10.4204/EPTCS.363.4
• Matthew Farrugia-Roberts, Bryn Jeffries and Harald Søndergaard. Programming to learn: Logic and computation from a programming perspective. In Proceedings of the 27th Annual Conference on Innovation and Technology in Computer Science Education (ITiCSE 2022), pages 311-317. ACM Press, 2022.
  PDF Bibtex DOI 10.1145/3502718.3524814
• Antonette Mendoza, Harald Søndergaard and Anne Venables. Making sense of a learning management system's quiz analytics in understanding students' learning difficulties. In N. Huda, D. Inglis, N. Tse and G. Town, editors, Proceedings of the 28th Annual Conference of the Australasian Association for Engineering Education (AAEE2017), pages 112-119. Australasian Association for Engineering Education, 2017.
  PDF Bibtex
• Harald Søndergaard and Raoul A. Mulder. Collaborative learning through formative peer review: Pedagogy, programs and potential. Computer Science Education 22 (4): 343-367, 2012.
  Bibtex DOI 10.1080/08993408.2012.728041
• Harald Søndergaard. Learning from and with peers: The different roles of student peer reviewing. In Proceedings of the 14th ACM SIGCSE Annual Conference on Innovation and Technology in Computer Science Education (ITiCSE 2009), pages 31-35. Association for Computing Machinery, New York, 2009.
  PDF Bibtex DOI 10.1145/3263191
• Rosemary L. Chang, Linda Stern, Harald Søndergaard and Roger Hadgraft. Places for learning engineering: A preliminary report on informal learning spaces. 2009 Research in Engineering Education Symposium. Palm Cove, Qld, Australia, 2009.
• Harald Søndergaard and Roger Hadgraft, editors. Proceedings of the 18th Conference of the Australasian Association for Engineering Education. Melbourne, Australia, 9-13 December 2007. ISBN 978-0-9757172-1-9.
  PDF Bibtex
• Alistair Moffat, Baden Hughes, Harald Søndergaard and Paul Gruba. Making connections: First year transition for computer science and software engineering students. In A. Young and D. Tolhurst, editors, Proceedings of the Seventh Australasian Computing Education Conference (ACE2005), Newcastle, Australia, 2005. Conferences in Research and Practice in Information Technology 42: 229-238.
  PDF Bibtex
• Harald Søndergaard and Doreen Thomas. Effective feedback to small and large classes. Proceedings of the 2004 ASEE/IEEE Frontiers in Education Conference, pages F1E-9 - F1E-14. Savannah GA, USA, 2004.
  PDF Bibtex DOI 10.1109/FIE.2004.1408573
• Paul Gruba, Alistair Moffat, Harald Søndergaard and Justin Zobel. What drives curriculum change? In R. Lister and A. Young, editors, Proceedings of the Sixth Australasian Computing Education Conference (ACE2004), Dunedin, New Zealand, January 2004. Conferences in Research and Practice in Information Technology 30: 109-117.
  PDF Bibtex
• Paul Gruba and Harald Søndergaard. A constructivist approach to communication skills instruction in computer science. Computer Science Education 11 (3): 203-219, 2001.
  Bibtex DOI 10.1076/csed.11.3.203.3833
• Paul Gruba and Harald Søndergaard. Transforming communication skills instruction: The conference approach. In J. Edwards, editor, Proceedings of the 23rd Australasian Computer Science Conference, Australian Computer Science Communications 22 (1): 88-94, IEEE Computer Society, 2000.
  PDF Bibtex DOI 10.1109/ACSC.2000.824385
• Linda Stern, Harald Søndergaard and Lee Naish. A strategy for managing content complexity in algorithm animation. In B. Manaris, editor, Proceedings of the Fourth Annual SIGCSE/SIGCUE Conference on Innovation and Technology in Computer Science Education (ITiCSE'99), pages 127-130. Association for Computing Machinery, New York, 1999.
  PDF Bibtex DOI 10.1145/305786.305891
• Roy Johnston, Alistair Moffat, Harald Søndergaard and Peter J. Stuckey. Low-contact learning in a first year programming course. In J. Rosenberg, editor, Proceedings of the First Australasian Conference on Computer Science Education, pages 19-26. ACM Press, 1996.
  PDF Bibtex DOI 10.1145/369585.369589