EuroProof Workshop
ek19, www.macs.hw.ac.uk/~ek19/In April, we organised a EuroProof network workshop at Edinburgh, on using machine learning and large language models in Mathematical proofs.
Welcome to my webpage!
I am a professor in Computer Science (AI and Verification) at the School of Mathematical and Computer Sciences (MACS), Heriot-Watt University, and the School of Electronics and Computer Science at the University of Southampton.
I do research in logic, programming languages, verification and AI.
Robotics SAIR Theme
ek19, www.macs.hw.ac.uk/~ek19/The National Robotarium and the Edinburgh Center for Robotics identified several high-priority research themes. We are happy to present the Research Theme SAIR: Safe and Secure AI for Robotics.
ARIA_Safeguarded_AI
ek19, www.macs.hw.ac.uk/~ek19/ARIA Safeguarded AI programme is running at full speed. Together with Bob Atkey, Matteo Capucci and Radu Mardare, I am a co-creator in the project ``Predicate Quantitative Logics for Safe Machine Learning"
DAIR CDT
ek19, www.macs.hw.ac.uk/~ek19/CDT D2AIR ( pronounced “dare”) is a joint 4-year PhD training programme offered by Heriot-Watt University and the University of Edinburgh. CDT-D2AIR will train students in the latest methods in AI, verification, design, and robotics, along with practical skills to ensure that robotic systems can be safely developed and deployed.
My recent and upcoming events:
- Research Project "Predicate Quantitative Logics for Safe Machine Learning", within the ARIA Safeguarded AI programme. Grant holders: B.Atkey and E.Komendantskaya, other researchers: M. Capucci and R. Mardare.
- Dependable and Deployable AI for Robotics (D2AIR) Centre for Doctoral Training, based at the Edinburgh Centre for Robotics (ECR), and jointly held by Heriot-Watt University and the University of Edinburgh. ECR includes the National Robotarium, a world-leading centre for Robotics and Artificial Intelligence based at Heriot-Watt’s Edinburgh campus, and the Bayes Centre, the University of Edinburgh 's Innovation Hub for Data Science and Artificial Intelligence.
- Research project AISEC: AI Secure and Explainable by Construction, . Funded as part of "Security for All in AI Enabled Society" call. Grant holders: E.Komendantskaya, D.Aspinall, B.Atkey, V.Rieser, B.Schafer; universities of Heriot-Watt, Edinburgh and Strathclyde.
- UKRI-funded ICASE PhD Scholarship with SLB Cambridge: Reasoning about Complex Systems that use Statistical Machine Learning and AI. Industrial lead: Michael John Williams, academic lead: Ekaterina Komendantskaya. Project Period: 2022- 2027.
- Imandra-funded PhD Scholarship at the Edinburgh Center for Robotics: Verification of Neural Networks in Imandra. Industrial lead: Grant Passmore, academic lead: Ekaterina Komendantskaya, PhD student: Remi Desmartin. Project Period: 2022-2026.
- Proof-Carrying Neuro-Symbolic Code. Invited talk at the International Conference on Functional Programming (ICFP'25) Singapore, October 2025.
- Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs. Invited talk at the International Conference on Formal Structures for Computation and Deduction (FSCD'25) Birmingham, UK, July 2025.
- Proof-Carrying Neuro-Symbolic Code. Invited talk at Computability in Europe (CiE'25), Lisbon, Portugal, July 2025.
- Proof-Carrying Neuro-Symbolic Code. Invited talk at Oxford Computer Science Conference 2025. Oxford, UK, June 2025
- Neural Network Verification is a Programming Language Challenge Workshop Formal Specification and Validation at Scale at Newton Institute for Mathematical Sciences, Cambridge. October 2024.
- Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs. Invited talk at Imperial College, London, 19 June 2024.
- Ensuring Neural Network Robustness: Problems and Opportunities. Invited talk at Beilstein Bozen Symposium 2024, Rudesheim, Germany. 2-6 June 2024.
- Mind Your Language: How to Make LLM Applications Trustworthy. Invited talk at Language and Computation Institute/ TAS Governance node in Edinburgh University, 22 April 2024.
- Invited participant at Dagstuhl Seminar 24121 Trustworthiness and Responsibility in AI – Causality, Learning, and Verification 17 - 22 March 2024.
- Neural Network Verification: Lessons Learnt from the Declarative Programming Perspective Invited talk at PADL'24, the 26th International Symposium on Practical Aspects of Declarative Languages, co-allocated with POPL'24 in London, in January 2024.
- Why? and How? of neural network verification. Agents, Interaction and Complexity Group, University of Southampton, 21 November 2023.
- Remi Desmartin, Omri Isac, Ekaterina Komendantskaya, Kathrin Stark, Grant Passmore and Guy Katz. A Certified Proof Checker for Deep Neural Network Verification in Imandra. International Conference on Interactive Theorem Proving, (ITP'25).
- Matthew L. Daggitt, Wen Kokke, Robert Atkey, Ekaterina Komendantskaya, Natalia Slusarz and Luca Arnaboldi. Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs. Invited paper at 10th International Conference on Formal Structures for Computation and Deduction (FSCD'25).
- Jairo Miguel Marulanda-Giraldo, Ekaterina Komendantskaya, Alessandro Bruni, Reynald Affeldt, Matteo Capucci and Enrico Marchioni. Quantifiers for Differentiable Logics in Rocq: Project Description. International Symposium on AI Verification (SAIV'25).
- Colin Kessler, Ekaterina Komendantskaya, Marco Casadio, Ignazio Maria Viola, Albaraa Ammar Othman, Alistair Malhotra and Robbie McPherson. Neural Network Verification for Gliding Drone Control: A Case Study. International Symposium on AI Verification (SAIV'25).
- E. Komendantskaya. Proof-Carrying Neuro-Symbolic Code. Invited Paper at Computability in Europe, (CiE'25).
- L. Cordeiro, M. Daggitt, J. Girard-Satabin, O. Isac, T. Johnson, G. Katz, E. Komendantskaya, A. Lemesle, E. Manino, A. Sinkarovs, and H. Wu. Neural Network Verification is a Programming Lan- guage Challenge. European Symposium on Programming (ESOP 2025).
- Casadio, M., Dinkar, T., Komendantskaya, E., Arnaboldi, L., Daggitt, M. L., Isac, O., Katz, G., Rieser, V. & Lemon, O. NLP verification: towards a general methodology for certifying robustness. European Journal of Applied Mathematics. p. 1-58 , 2025.
- R. Flood, M. Casadio, D. Aspinall and E. Komendantskaya. Formally Verifying Robustness and Generalisation of Network Intrusion Detection Models. ACM/SIGAPP Symposium On Applied Computing (SAC 2025).
- Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Ślusarz, Kathrin Stark. Taming Differentiable Logics with Coq Formalisation. Interactive Theorem Proving (ITP) Tbilisi, Georgia, September 2024. LIPICS 309: 1-19, 2024.
- Haoze Wu, Omri Isac, Aleksandar Zeljic, Teruhiro Tagomori, Matthew L. Daggitt, Wen Kokke, Idan Refaeli, Guy Amir, Kyle Julian, Shahaf Bassan, Pei Huang, Ori Lahav, Min Wu, Min Zhang, Ekaterina Komendantskaya, Guy Katz, Clark W. Barrett: Marabou 2.0: A Versatile Formal Analyzer of Neural Networks. Computer-Aided Verification (CAV), Montreal, Canada, 22-27 July 2024.
- Parth Padalkar, Natalia Slusarz, Gopal Gupta, Ekaterina Komendantskaya, A Neurosymbolic Framework for Bias Correction in Convolutional Neural Networks. International Conference on Logic Programming, ICLP 2024. Journal Proceedings in the joutnal of Theory and Practice of Logic Programming.
- ITP 2026: 17th International Symposium on Interactive Theorem Proving. Serving as PC Chair.
- FLOPS 2026: 18th International Symposium on Functional and Logic Programming. Serving as PC Chair.
- POPL 2026: the 53rd ACM SIGPLAN Symposium on Principles of Programming Languages
- CPP 2025: Certified Proofs and Programs, affiliated with POPL'25
- SAIV 2025: the 8th International Symposium on AI Verification affiliated with CAV'25
- March 2024 April 2025: a member of the Editorial Board of Science of Computer Programming
- Haskell 2024: the Haskell Symposium affiliated with ICFP'24
- SAIV 2024: the 7th International Symposium on AI Verification affiliated with CAV'24
- LOPSTR 2024: the 34th Symposium on Logic-Based Program Synthesis and Transformation
- ICFP 2024: the 29th ACM SIGPLAN International Conference on Functional Programming
- TYPES 2024: the 30th International Conference on Types for Proofs and Programs
- FLOPS 2024: 17th International Symposium on Functional and Logic Programming
2025 Running Grants:
2024 -2025 Invited talks and tutorials:
2024-2025 Research papers:
2024 -- 2026 PC membership:
My selected publications (full list is given here):
- Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Ślusarz, Kathrin Stark. Taming Differentiable Logics with Coq Formalisation. Interactive Theorem Proving (ITP) Tbilisi, Georgia, September 2024.
- M. Casadio, E. Komendantskaya, M. L. Daggitt, W. Kokke, G. Katz, G. Amir and I. Refaeli: Neural Network Robustness as a Verification Property: A Principled Case Study. International conference on Computer-Aided Verification CAV'22 (Part of FLOC'22).
- A.Hill, E. Komendantskaya, M. Daggitt and R.Petrick. Actions You Can Handle: Dependent Types for AI Plans. The Workshop on Type-Driven Development 2021 (co-allocated with ICFP21).
- Wen Kokke, Ekaterina Komendantskaya, Daniel Kienitz, Robert Atkey, and David Aspinall. Neural Networks, Secure by Construction: An Exploration of Refinement Types. In APLAS'20, the The 18th Asian Symposium on Programming Languages and Systems.
- H. Basold, E. Komendantskaya, Y. Li Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses. ESOP 2019 (28th European Symposium on Programming), 8-11 April 2019, Prague.
- E.Komendantskaya and J.Power Logic Programming: Laxness and Saturation. Journal of Logical and Algebraic Methods in Programming Volume 101, December 2018, Pages 1-21.
- E.Komendantskaya and J.Heras Proof Mining with Dependent Types, Conference on Intelligent Computer Mathematics, CICM'17 in Edinburgh, 17-21 July 2017, Edinburgh.
- P.Fu, E.Komendantskaya, T.Schrijvers, A.Pond. Proof Relevant Corecursive Resolution Thirteenth International Symposium on Functional and Logic Programming FLOPS'2016, Japan, 3-6 March 2016. Springer LNCS 9613, 126-143.
- E.Komendantskaya, J.Power and M.Schmidt. Coalgebraic Logic Programming: from Semantics to Implementation. Journal of Logic and Computation, 26(2), 745-783, 2016.
- J.Heras, E.Komendantskaya, M.Johansson, and E.Maclean. Proof-Pattern Recognition and Lemma Discovery in ACL2 19th International conference on Logic for Programming Artificial Intelligence and Reasoning, LPAR'13, Stellenbosch, South Africa, 15-19 December 2013. Springer LNCS 8312, pp. 389-406, 2013.
- Y. Bertot and E. Komendantskaya. Inductive and Coinductive Components of Corecursive Functions in Coq, CMCS'08, the 9th International Workshop on Coalgebraic Methods in Computer Science, Budapest, Hungary, 4 - 6 April, 2008. ENTCS 203/5 pp.25--47, 2008.