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, a federated Logic Conference, in Lisbon in July 2026. We are inviting good-quality submissions devoted to theory and applications of interactive theorem proving!

See ITP official webpage »

FLOPS'26, Functional and Logic Programming

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

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

Consider submitting to the 18th International Symposium on Functional and Logic Programming May 26-28, 2026, Akita, 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 Invited talks and tutorials:

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 Research papers:

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:

ITP 2026: the 17th International Symposium on Interactive Theorem Proving. Serving as PC Chair.
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):

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.