Dr. Zoltan A. Kocsis

Adjunct Lecturer at UNSW Sydney. Mathematician and educator based in Sydney, Australia, with contributions to category theory, combinatorics, proof theory and nonstandard analysis. Consultant with extensive experience in software verification (security, safety and reliability) and in stochastic optimization.

Education

PhD in Mathematics (2016-2019)

Supervised by Prof. Alexandre Borovik
Thesis: Development of Group Theory in the Language of Internal Set Theory
The University of Manchester, Oxford Rd, Manchester M13 9PL, UK

BSc Hons. in Mathematics and Computer Science (2013-2016)

Scottish Bachelor's degree with first class honors; multiple academic prizes and awards
Thesis: Evaluating pseudo-random number generators using topological data analysis
University of Stirling, Stirling FK9 4LA, Scotland UK

Work Experience

Lecturer in Formal Methods, University of New South Wales (October 2022 - June 2023)

Research and teaching position at the School of Computer Science & Engineering of UNSW, a Group of Eight research university based in Sydney, Australia.
Conducting independent research in mathematical techniques for the formal verification of software.
Development of rigorous mathematical techinques for operating system security, safety and reliability.
Teaching and learning design, development and delivery at undergraduate and postgraduate level; supervision of research students/interns at the Trustworthy Systems group.

Research Assoc., University of New South Wales (December 2021 - October 2022)

Research position at the Trustworthy Systems group at UNSW, a Group of Eight research university based in Sydney, Australia.
Research and development of computer-aided verification techniques for the seL4 kernel and the seL4 Core Platform (SAT/SMT).
Advancement of rigorous mathematical techinques for proofs of software security, safety and reliability.
Teaching and learning design, development and delivery at undergraduate level (as lecturer-in-charge); co-supervision of research students/interns at the Trustworthy Systems group.

Senior Proof Eng., CSIRO Officer (October 2019 - November 2021)

Research engineer position at CSIRO, the Australian federal government agency responsible for scientific research.
Development, maintenance, and improvement of formal models; proofs of software security, safety and reliability using interactive theorem proving technology such as Isabelle/HOL and HOL4.
Research and development of the graph refinement / binary verification proofs of the seL4 operating system, using computer-aided verification technology (SAT/SMT).
Trustworthy Systems Research Group: CSIRO Data61, Kensington site, University of New South Wales, Kensington NSW 2033, Australia

PhD in Mathematics (September 2016 - October 2019)

Research on the applications of the techniques of Nonstandard Analysis and Internal Set Theory in Abstract Algebra. Novel results generalizing previous work by E. I. Gordon and B. Zilber.
Development of a new formalism for computer verification of proofs in Nonstandard Analysis, expressed in Martin-Löf Type Theory. Correctness of main results verified using the Agda proof assistant.
Research in probabilistic degree of satisfiability in group theory, yielding criteria to identify which equations hold in a finite index subgroup precisely if they have positive degree of satisfiability.
Independent teaching, assisting undergraduates with performing required tasks in laboratory settings, marking and record-keeping. Experience with event organization in academic settings.

Research Intern, YCCSA (June 2015 - August 2015)

Undertake research on hyper-heuristics for proof search, and progress associated research projects towards journal publication.
York Cross-disciplinary Centre for Systems Analysis, at the University of York, Deramore Lane, York YO10 5GH, UK

Research Intern, Agilent (June 2014 - September 2014)

Develop research software for performance optimization of Apache Spark source code.
Prepare research papers to be published in academic literature, under the supervision of Dr. Jerry Swan.
Work performed at University of Stirling, Stirling FK9 4LA, UK, on an Agilent Technologies grant ('Database Query Optimization').

Academic Activities

Invited/Recent talks

Invited speaker, Constructive Mathematics: Foundation and Practice 2023, Nis, Serbia, 26 Jun 2023
Invited speaker, LMS Prospects in Mathematics 2019, on Proof Theory and Topology, Lancaster UK, 6 Sep 2019
6th International School and Workshop on Proof Theory, on A structural approach to higher-order connectives, Birmingham, UK, 13 Sep 2024
Budapest Type Theory Seminar, invited talk on The probability of Excluded Middle, Budapest, Hungary, 16 Sep 2024
ACM Asia-Pacific Workshop on Systems Conference, on First steps in verifying the seL4 Core Platform (joint work, presented by M. Paturel), Seoul, South Korea, 23 Jul 2023
seL4 Summit 2022 Conference, on Verifying the Core Platform, Munich, Germany, 10 Oct 2022
UNSW Trustworthy Systems Seminar, on Degree of Associativity: Supercharge your Property-Based Tests, Kensington NSW, Australia, 02 May 2022
Applied Category Theory 2021 Conference, on Treewidth via Spined Categories, Cambridge, UK, 12-16 Jul 2021
Australian Category Seminar, on Spined Categories, Centre of Australian Category Theory, North Ryde NSW, Australia, 23 Jun 2021
CSIRO Trustworthy Systems Seminar, on Degree of satisfiability in Groups and Lattices, Eveleigh NSW, Australia, 26 Apr 2021
BCTCS 2021 on Spined categories: generalizing tree-width beyond graphs (joint work, presented by B. Bumpus), Liverpool, UK, 31 Mar 2021
Budapest Type Theory Seminar, on Internal Type Theory, Budapest, Hungary, 30 June 2020
UNSW/CSIRO joint Trustworthy Systems Seminar, on Pseudo-random sequences and Homology, Kensington NSW, Australia, 23 Mar 2020
UoM Logic Seminar, on Extension of Group Actions via Internal Set Theory, Manchester, UK, Mar 2019
Manchester Research Students Conference (MRSC 2018), on Results on Degree of Satisfiability, Manchester, UK, 28 Sep 2018

Organization

Organizing Committee, UNSW Computing Research Expo 2022
Program Committee, Applied Category Theory Conference 2022
Organizer, British Postgraduate Model Theory Conference 2019
Refereeing experience, articles in logic and automated reasoning in premier international journals and conferences.

Teaching and Supervision

COMP3141 "Software System Design and Implementation": Lecturer-in-charge, University of New South Wales, 2022 2nd Term. The course is an introduction to rigorous mathematical methods for the design and implementation of software systems (mathematically structured programming), using the Haskell programming language.
Proof Theory Lecture Course: Instructor, University of Manchester, 2018-19 1st Semester. Lecture course for students in Mathematics and in Philosophy, covering Gentzen's cut-elimination theorem, Herbrand's theorem, Takeuti's conjecture and select applications.
MATH36032 "Problem-solving by Computer": Teaching Assistant, University of Manchester, 2017-18 2nd Semester. The course unit develops skills in translating mathematical ideas into MATLAB programs, thereby using the computer as a tool to investigate and solve mathematical problems.
MATH20302 "Introduction to Logic": Teaching Assistant, University of Manchester, 2016-17 2nd Semester. The course unit aims to introduce the student to the idea of formalizing arguments, both semantically and syntactically, and to the fundamental connection between these approaches.
MATH20212 "Algebraic Structures 2": Teaching Assistant, University of Manchester, 2016-17 2nd Semester. The course unit unit aims to introduce the algebraic structures of rings and fields; describe the quotient structure and its connection with homomorphisms of rings; present important examples rings and develop some of their properties.
MATH20101 "Real and Complex Analysis": Teaching Assistant, University of Manchester, 2016-17 1st Semester. The course unit unit aims to introduce the basic ideas of real analysis (continuity, differentiability and Riemann integration) and their rigorous treatment, followed by complex analysis, with particular emphasis on Cauchy's Theorem and the calculus of residues.
MATH19861 "Mathematics 0N1": Teaching Assistant, University of Manchester, 2016-17 1st Semester; 2017-18 1st Semester; 2018-19 1st Semester. The course unit aims to provide a basic course in pure mathematical topics for members of the foundation year.
CSCU9Y4 "Programming Language Paradigms": Lab Demonstrator, University of Stirling, 2016. The course is an introduction to programming paradigms, including logic programming and Prolog.

Other Events

International Summer School on Linear Logic and Geometry of Interaction, on inv. Dr. Claudia Faggian, Inria LOGOI, Turin, Italy, 2013.
Midlands Graduate School, on inv. Prof. Achim Jung, University of Birmingham, April 2016, Birmingham, UK.
Autumn School "Proof and Computation", on inv. Dr. Chuangjie Xu, LMU Munich, September 2017, Herrsching, Germany.
Supervision and research assessment: Kevin Tran (UNSW ToR supervisor, 2022); Mathieu Paturel (UNSW ToR supervisor, 2023), Kurt Wu (UNSW MSc assessor, 2024)

Awards and Honors

Recipient, CSIRO SCS Engineering and Technology Award, awarded for Translation Validation of seL4 on the RISC-V Architecture, 2021
Recipient, IBM Prize, awarded for Results on Degree of Satisfiability, 2018
Recipient, Ede & Ravenscroft Prize for Academic Excellence, 2015/2016
Recipient, School Prize for Research-based Learning, University of Stirling, awarded annually at the discretion of the examiners for outstanding performance in mathematics, 2015/2016
Recipient, Computing Science 2nd Year Prize, University of Stirling, awarded annually to the second-year student with the best overall performance across all Computing Science modules, 2014/2015
Recipient, Dept. Research-based Learning Prize, Undergraduate, University of Stirling, 2014/2015

Software Skills

Software engineering experience, with contributions to large code bases written in the following programming languages: C, Haskell, Java, Python, Scala
Experience with and contributions to large proof bases verified using automated theorem provers: Agda, Isabelle/HOL, HOL4, and contributions to the HOL4 main repository.
Experience with development of research scientific software for binary verification / translation validation, with cyber-security applications.
Experience with optimization algorithms and tools, including evolutionary algorithms, relational algebra optimizers, and SAT/SMT solvers, applied to large commercial projects and code bases.
Web development experience: graphic design experience, full-stack development experience in the Elm programming language. For ref. see modeltheory.uk or email for further references.

Research Articles

B. M. Bumpus, Z. A. Kocsis: Degree of satisfiability in Heyting algebras. arXiv:2110.11515, to appear in Journal of Symbolic Logic (2024)
Z. A. Kocsis: Proof-theoretic methods in quantifier-free definability. arXiv:2310.03640, submitted (2023)
Z. A. Kocsis: Apartness relations between propositions. arXiv:2209.03920, submitted (2023)
B. M. Bumpus, Z. A. Kocsis, J. E. Master: Structured Decompositions: Structural and Algorithmic Compositionality. arXiv:2207.06091, submitted (2022)
B. M. Bumpus, Z. A. Kocsis: Spined categories: generalizing tree-width beyond graphs. arXiv:2104.01841, to appear in European Journal of Combinatorics (2021)
Z. A. Kocsis: Degree of satisfiability of some special equations. arXiv:2002.01773, submitted to International Journal of Algebra and Computation (2020)
A. E. I. Brownlee, R. Senington, J. Swan and Z. A. Kocsis: Conflict-free routing of multi-stop warehouse trucks. Optimization Letters 14(6): 1459-1470 (2020)
Z. A. Kocsis: Development of group theory in the language of Internal Set Theory. University of Manchester administered thesis, Ph. D. (2019)
Z. A. Kocsis, J. Swan: Genetic Programming and Proof Search for Automatic Improvement. Journal of Automated Reasoning 60(2): 157-176 (2018)
Z. A. Kocsis: Hat Problems in Internal Set Theory (meant for ThEdu '20, cancelled due to pandemic, in prep.) (2020)
J. Swan, K. Krawiec, Z. A. Kocsis: Stochastic synthesis of recursive functions made easy.... Genetic Programming and Evolvable Machines 20(3): 327-350 (2019)
J. Swan, K. Krawiec, Z. A. Kocsis: Stochastic program synthesis via recursion schemes. GECCO (Companion) 2019: 35-36
Z. A. Kocsis, J. Swan: Dependency Injection for Programming by Optimization, arXiv:1707.04016, in prep., 2017
Z. A. Kocsis, J. H. Drake, D. Carson, J. Swan: Automatic Improvement of Apache Spark Queries using Semantics-preserving Program Reduction. GECCO (Companion) 2016: 1141-1146
N. Burles, J. Swan, E. Bowles, A. E. I. Brownlee, Z. A. Kocsis, N. Veerapen: Embedded Dynamic Improvement. GECCO (Companion) 2015: 831-832
(Burke et al., 24 coauthors) A Research Agenda for Metaheuristic Standardization. In: Proceedings of the Eleventh Metaheuristics International Conference (MIC) 2015.
Z. A. Kocsis, A. E. I. Brownlee, J. Swan, R. Senington: Haiku - a Scala Combinator Toolkit for Semi-automated Composition of Metaheuristics. SSBSE 2015: 125-140
N. Burles, E. Bowles, A. E. I. Brownlee, Z. A. Kocsis, J. Swan, N. Veerapen: Object-Oriented Genetic Improvement for Improved Energy Consumption in Google Guava. SSBSE 2015: 255-261
Z. A. Kocsis, A. Lisitsa: The representative metaheuristic design pattern. GECCO (Companion) 2014: 1435-1436
Z. A. Kocsis and J. Swan. Asymptotic Programming with Type Functors and Catamorphisms. In Proc. of Parallel Problem Solving from Nature (PPSN XIV). Ed. by Colin Johnson, Krzysztof Krawiec, and and Michael O’Neill Alberto Moraglio. Ljubljana, Slovenia, 2014.
Z. A. Kocsis, G. Neumann, J. Swan, M. G. Epitropakis, A. E. I. Brownlee, S. O. Haraldsson, E. Bowles: Repairing and Optimizing Hadoop hashCode Implementations. SSBSE 2014: 259-264

Personal Skills

Nationality: Hungarian. Acquired indefinite leave to enter the United Kingdom via the EU Settlement Scheme. Legally eligible for paid employment in Australia, the European Union, and the United Kingdom.
Fluent in English and Hungarian. Some educational experience in the Spanish language.
Professional memberships: Member of the British Computer Society, Member of the Proof Society.
Former member of Manchester Orators (2017-2019), a chartered club for development of public speaking, presentation and leadership skills.