Chelsea Edmonds
Department of Computer Science
Research Associate in Formal Modelling Verification
Full contact details
Department of Computer Science
Regent Court (DCS)
211 Portobello
Sheffield
S1 4DP
- Profile
-
I'm a postdoctoral researcher in formal verification, currently working on the verification and formal modelling of security properties for programs running on advanced concurrent architectures (as part of the COVERT EPSRC grant) using the proof assistant Isabelle/HOL. Previously, I completed my PhD in formalised mathematics at the University of Cambridge (supervised by Prof. Lawrence Paulson), fully funded by a Cambridge Australia Scholarship. My PhD research resulted in five peer-reviewed publications, including a distinguished paper, and earned a British Federation of Women Graduates Academic Award. Before my PhD, I studied for a Bachelor of Science (Mathematics) and Bachelor of Engineering (Software), graduating with first class honours and a university medal from the University of Queensland, and worked as a Software Engineer.
Beyond my research, I'm a passionate educator (AFHEA) and ambassador for STEM outreach and women in computer science. I've been honoured to receive several awards in recognition of my leadership and service in this space, including a Women in Technology Young Achiever Award and GradConnection Top100 Future Leader Australia award in 2017.
- Research interests
-
- Theorem proving
- Formal methods
- Verification
- Security
- Formalised mathematics
- Publications
-
Journal articles
- Formalising Szemerédi’s regularity lemma and Roth’s theorem on arithmetic progressions in Isabelle/HOL. Journal of Automated Reasoning, 67. View this article in WRRO
Chapters
- A Modular First Formalisation of Combinatorial Design Theory, Lecture Notes in Computer Science (pp. 3-18). Springer International Publishing
Conference proceedings papers
- Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemma. Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs
- A formalisation of the Balog–Szemerédi–Gowers theorem in Isabelle/HOL. CPP 2023: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs (pp 225-238). Boston, MA, USA, 16 January 2023 - 16 January 2023. View this article in WRRO
- Formalising Fisher’s Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics. Leibniz International Proceedings in Informatics
Preprints
- Formal Probabilistic Methods for Combinatorial Structures using the
Lovász Local Lemma.
- Formalising Szemerédi's Regularity Lemma and Roth's Theorem on
Arithmetic Progressions in Isabelle/HOL.
- Formalising Fisher's Inequality: Formal Linear Algebraic Proof
Techniques in Combinatorics.
- A Modular First Formalisation of Combinatorial Design Theory.
- Formalising Szemerédi’s regularity lemma and Roth’s theorem on arithmetic progressions in Isabelle/HOL. Journal of Automated Reasoning, 67. View this article in WRRO
- Research group