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. I lead the Lab for AI and Verification


Vehicle Tutorials

ek19, www.macs.hw.ac.uk/~ek19/

Vehicle is a functional domain specific language for writing specifications of neural network properties, and compiling them down either for verification with neural network solvers or for property-driven training in Python. Interested to join the Vehicle team? -- contact me.

See also the Vehicle tutorial webpage »

Edinburgh Center for Robotics


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:

Most of my time, I work with my research team LAIV. On its webpage, you will find more information about our current activities, seminars, researchers and research students. This page gives a more structured but more static snapshot of those activities.

    2024 Running Grants:

  • 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, PhD student: Ben Coke. 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.
  • 2023 -2024 Invited talks and tutorials:

  • 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.
  • Neural Network Verification with Vehicle, 18 July 2023, 22-24 August 2023, 8 September 2023: tutorial at FOMLAS'23 in Paris, VETSS Summer School in Surrey, ICFP'23 Tutorial Fest in Seattle.
  • Integrated Neural Network Verification with Vehicle. Invited talk, Trustworthy Autonomous Systems Verifiability Node (TAS), 18 May 2023
  • Integrated Neural Network Verification with Vehicle. Invited talk at Copenhagen University, 23 May 2023
  • Safe Machine Learning for Robotics? Invited talk at the Edinburgh Centre for Robotics & the Alan Turing Institute Symposium "Bridging International Robotics and AI Grand Challenges: working with the Japanese MOONSHOT Initiative". O5 June 2023
  • Speaker at NeSyMAS Panel. NeSyMAS 2023: Neuro-symbolic AI for Agent and Multi-Agent systems workshop, at AAMAS, London. 30 May 2023
  • 2023-2024 Research papers:

  • Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Ślusarz, Kathrin Stark. Taming Differentiable Logics with Coq Formalisation. Interactive Theorem Proving (ITP) Tbilisi, Georgia, September 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.
  • Vaishak Belle, Michael Fisher, Alessandra Russo, Ekaterina Komendantskaya, Alistair Nottle: Neuro-Symbolic AI + Agent Systems: A First Reflection on Trends, Opportunities and Challenges. AAMAS Workshops, London, 30 May 2023: 180-200
  • Natalia Slusarz, Ekaterina Komendantskaya, Matthew L. Daggitt, Robert J. Stewart, Kathrin Stark: Logic of Differentiable Logics: Towards a Uniform Semantics of DL. LPAR 2023, 24th International Conference on Logic for Programming, AI and Reasoning.
  • Matthew L. Daggitt, Robert Atkey, Wen Kokke, Ekaterina Komandantskaya, Luca Arnaboldi. Compiling higher-order specifications to SMT solvers: how to deal with rejection constructively. Certified Proofs and Programs. CPP'23. Boston, USA, 16-17 January 2023.
  • Matthew Daggitt, Wen Kokke, Ekaterina Komendantskaya, Robert Atkey, Luca Arnaboldi, Natalia Slusarz, Marco Casadio, Ben Coke and Jeonghyeon Lee. The Vehicle Tutorial: Neural Network Verification with Vehicle. FOMLAS 2023: 6th Workshop on Formal Methods for ML-Enabled Autonomous Systems Affiliated with CAV 2023. Easychair Proceedings.
  • Marco Casadio, Luca Arnaboldi, Matthew L. Daggitt, Omri Isac, Tanvi Dinkar, Daniel Kienitz, Verena Rieser, Ekaterina Komendantskaya: ANTONIO: Towards a Systematic Method of Generating NLP Benchmarks for Verification. FOMLAS 2023: 6th Workshop on Formal Methods for ML-Enabled Autonomous Systems Affiliated with CAV 2023. Easychair Proceedings.
  • Remi Desmartin, Omri Isac, Grant O. Passmore, Kathrin Stark, Guy Katz, Ekaterina Komendantskaya: Towards a Certified Proof Checker for Deep Neural Network Verification. LOPSTR'2023, October 2023, Cascais, Portugal.
  • Luca Arnaboldi, David Aspinall, Ronny Bogani, Burkhard Schafer, Scott Herman, Jonathan Protzenko, Ekaterina Komendantskaya, Yue Li , Remi Desmartin. Formalising Criminal Law in Catala. PRoLaLa, POPL Workshop on Programming Languages and the Law 2023.
  • 2023 - 2024 PC membership:

  • From March 2024: 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
  • POPL 2023: the 50th ACM SIGPLAN Symposium on Principles of Programming Languages
  • PPDP 2023: 25th International Symposium on Principles and Practice of Declarative Programming
  • PADL 2023: The 25th International Symposium on Practical Aspects of Declarative Languages
  • CiE 2023, the 19th conference on Computability In Europe 2023
  • HCVS2023 , the 10th workshop on Horn Clauses for Verification and Synthesis
  • FOMLAS 2023: 6th Workshop on Formal Methods for ML-Enabled Autonomous Systems Affiliated with CAV 2023
  • TYPES 2023: the 29th International Conference on Types for Proofs and Programs, proceedings and post-proceedings
  • PRoLaLa: POPL Workshop on Programming Languages and the Law 2023
  • MiniKanren 2023: The miniKanren and Relational Programming Workshop at ICFP 2023

My selected publications (full list is given here):