Research interests:

  1. Computational Logic and Declarative Programming Languages,
  2. Automated and Interactive Theorem Provers,
  3. Verification for AI: how to prove AI algorithms (e.g. learning in neural networks) correct and secure,
  4. AI for Verification: applications of statistical machine learning in theorem proving,
  5. Induction and Coinduction, Recursion and Corecursion in logic and functional programming,
  6. Categorical Logic and Categorical Semantics of Computations.

Current Research grants (PI or CoI):

  1. Co-creator in the 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.
  2. I am a CoI in the 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. Directors: Ron Petrick and Ram Ramamoorthy. PhD students to be funded: 88. Grant Duration: 1/07/2024 - 31/12/2032.
  3. PI in EPSRC-funded 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, Strathclyde. Grant duration: 01/09/20 -- 01/05/2025.
  4. First supervisor in 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 duration: 2022- 2027.
  5. First supervisor in 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 duration: 2022-2026.

    6. Previous Research grants (as a PI):

  6. Research project Neural Network Verification: in search of the missing spec. Funded by UK Research Institute in Verified Trustworthy Software Systems (VETSS) as part of the "Safe and Secure Software Systems" call. Grant holders: E.Komendantskaya and G.Katz, named RAs: Natalia Slusarz and Warrick Macmillan. Grant period: 01 April 2021 -- 01 April 2022.
  7. UK Research Institute in Verified Trustworthy Software Systems (VETSS)-funded research project CONVENER: Continuous Verification of Neural Networks. Funded as part of "Digital Security Through Verification" call. Grant holders: E.Komendantskaya and D.Aspinall, named RAs: Wen Kokke and Daniel Kienitz. Grant period: 01/04/20 -- 31/03/2021.
  8. National Cyber Security Center (NCSC)-funded research project SecCon-NN: Neural Networks with Security Contracts - towards lightweight, modular security for neural networks. Funded as part of NCSC "Security for AI" call. Grant holders: E.Komendantskaya and D.Aspinall. Grant period: 01/11/19 -- 31/03/2020.
  9. The Integration and Interaction of Multiple Mathematical Reasoning Processes. EPSRC Platform Grant EP/N014758/1 Grant holders: A. Ireland (PI), D. Aspinall, A. Bundy, A. Smaill, J. Fleuriot, P. Jackson (Edinburgh), G. Michaelson, K. Komedantskaya, Fiona McNeill (Heriot-Watt), S. Colton, J. Gow (Goldsmiths College). Grant period: 01/11/15 to 31/10/19.

  10. EPSRC grant Coalgebraic Logic Programming for Type Inference: parallelism and corecursion for a new generation of programming languages, 2013-2017. Joint with John Power, University of Bath.

  11. SICSA Industrial "Proof of Concept" grant Machine-Learning for Industrial Theorem Proving, 2013-2014. Joint with Jonathan Heras.

  12. EPSRC First Grant scheme; project title Machine-Learning Coalgebraic Automated Proofs, 2012-2014.

    Associated with this grant is the project on ML4PG, on data mining proofs in Coq via Proof General interface.

  13. EPSRC Postdoctoral Research Fellowship in Theoretical Computer Science; project title and web-page Computational Logic in Artificial Neural Networks, 2008-2011.

Smaller research grants, in parallel to the above:

INRIA Postdoctoral experience

I did my first postdoc in INRIA Sophia-Antipolis, France. For 13 months, I had a pleasure to be a member of the Research Team Marelle. Marelle is one of the world's leading research units for development of automated higher-order proof assistant Coq. My Postdoc was entitled Automatic Proofs for Recursive and Co-recursive Formal Descriptions of Algorithms. PI: Yves Bertot. Funded by INRIA CORDI Fellowship Scheme.

PhD Thesis

I did my PhD at the Department of Mathematics,
University College, Cork (UCC), Ireland.

My PhD thesis is entitled Learning and Deduction in Neural Networks and Logic, 2007.