Congratulations to Amy on passing her PhD viva!
Many congratulations to Amy Stell who passed her PhD viva with minor corrections!
Amy’s PhD thesis [1] entitled “Trustworthy Machine Learning for High-Assurance Systems” presents an approach for modelling and formally verifying neural networks in Isabelle/HOL. This is an important step to enabeling the use of neural networks in safety-critical or security-critical applications. During his PhD, Amy published several conference publications and entries of the Archive of Formal Proofs [5].
Well done Amy!
Amy will stay in our group, working on formal methods for enterprise systems; and, of course, she will also continue to work on formal methods for AI.
References §
[1]
A. Stell, “Trustworthy machine learning for high-assurance systems,” PhD thesis, University of Exeter, 2025. https://hdl.handle.net/10779/exe.30610607/
[2]
A. D. Brucker and A. Stell, “Verifying feedforward neural networks for classification in Isabelle/HOL,” in Formal methods (FM 2023), M. Chechik, J.-P. Katoen, and M. Leucker, Eds. Heidelberg: Springer-Verlag, 2023. doi: 10.1007/978-3-031-27481-7_24. Author copy: http://logicalhacking.com/publications/brucker.ea-feedforward-nn-verification-2023/
[3]
A. D. Brucker and A. Stell, “Formalizing neural networks,” Archive of Formal Proofs, 2025. https://isa-afp.org/entries/Neural_Networks.html, Formal proof development
[4]
A. D. Brucker, T. Cameron-Burke, and A. Stell, “Formally verified interval arithmetic and its application to program verification,” 2024. doi: 10.1145/3644033.3644370. Author copy: http://logicalhacking.com/publications/brucker.ea-interval-arithmetic-2024/
[5]
A. D. Brucker and A. Stell, “(Extended) Interval Analysis,” Archive of Formal Proofs, Jan. 2024. https://www.isa-afp.org/entries/Interval_Analysis.html, Formal proof development. Author copy: http://logicalhacking.com/publications/brucker.ea-interval-arithmetic-afp-2024/