Ekaterina Komendantskaya

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.

Vehicle

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"

See also ARIA webpage »

Edinburgh Center for Robotics

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.

Read More »

My recent and upcoming events:

    2025 Running Grants:

  • 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.

    • 2024 -2025 Invited talks and tutorials:

  • Invited talk at ICFP'25 Proof-Carrying Neuro-Symbolic Code.. Singapore, October 2025.
  • Invited talk at FSCD'25 Proof-Carrying Neuro-Symbolic Code.. Birmingham, UK, July 2025.
  • Invited talk at CiE'25 Proof-Carrying Neuro-Symbolic Code. Lisbon, Portugal, July 2025.
  • Invited talk at Oxford Computer Science Conference 2025 Proof-Carrying Neuro-Symbolic Code.. Oxford, Uk, June 2025
  • Neural Network Verification is a Programming Lan- guage Challenge Workshop Formal Specification and Validation at Scale at Newton Institute for Math. Sci., 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.

    • 2024-2025 Research papers:

  • E. Komendantskaya. Proof-Carrying Neuro-Symbolic Code. Invited Ppaer 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.

    • 2024 -- 2026 PC membership:

  • 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

My selected publications (full list is given here):