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!

ITP

Interactive Theorem Proving

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

Monday, 08^th December 2025 @20:16:33

ITP'26 is held as part of FLOC'26, the Federated Logic Conference, in Lisbon in July 2026. We have an exciting program of research talks, as well as special sessions on the use of AI in mathematics and formal proofs.

See ITP official webpage »

FLOPS'26, Functional and Logic Programming

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

Monday, 10^th November 2025 @20:32:10

Consider submitting to the 18th International Symposium on Functional and Logic Programming May 26-28, 2026, Tskuba, Japan

See FLOPS official webpage »

ARIA Safeguarded AI

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

Sunday, 20^th April 2025 @17:25:00

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/

Sunday, 26^th May 2024 @18:15:00

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:

2026 Running Research 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.
UKRI-funded ICASE PhD Scholarship with SLB Cambridge: Optimizing ML models for satisfying logical constraints. Industrial lead: Michael John Williams, academic lead: Ekaterina Komendantskaya.

2025 - 2026 Invited talks and tutorials:

Compositional Neuro-Cyber-Physical System Verification in the Interactive Theorem Prover of your Choice. Invited talk at the Brighton University, 08 July 2026.
Safe AI for Robotics. UK Robotics Summer School 2026, 25 June 2026.
Compositional Neuro-Cyber-Physical System Verification in the Interactive Theorem Prover of your Choice. Invited talk at the Oxford Verification Seminars, 14 May 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

2025 - 2026 Research papers:

Alistair Sirman, Fleur Conway, Jessica Ciupa, Gusts Gustavs Grinbergs, Ekaterina Komendantskaya, Thai Son Hoang, Michael Rawson, Alessandro Bruni, Vaishak Belle, Michael John Williams. Vancomycert: A Certified Neuro-Symbolic Drug Delivery System (Case Study). Symposium on AI Verification (SAIV'26).
Matthew Daggitt, Ekaterina Komendantskaya, Alistair Sirman, Alessandro Bruni, Samuel Teuber, Joshua Smart, Grant Passmore. Compositional Neural-Cyber-Physical System Verification in the Interactive Theorem Prover of Your Choice. International Conference on Functional Programming (ICFP'26).
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).

2025 - 2026 PC membership:

FSCD 2027: the 12th International Conference on Formal Structures for Computation and Deduction.
ITP 2026: the 17th International Symposium on Interactive Theorem Proving. Serving as PC Chair.
SAIV 2026: the 9th International Symposium on AI Verification affiliated with CAV'26
NeuS 26: 3rd International Conference on Neuro-Symbolic Systems 2026
FLOPS 2026: the 18th International Symposium on Functional and Logic Programming. Serving as PC Chair.
CAV 2026: the 38th International Conference on Computer Aided Verification
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

My selected publications (full list is given here):

M. Daggitt, E. Komendantskaya, A. Sirman, A. Bruni, S. Teuber, J. Smart, G. Passmore. Compositional Neural-Cyber-Physical System Verification in the Interactive Theorem Prover of Your Choice. International Conference on Functional Programming (ICFP'26).
R. Affeldt, A. Bruni, E. Komendantskaya, N. Slusarz, K. 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).
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.
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.