Research interests:
- Computational Logic and Declarative Programming Languages,
- Automated and Interactive Theorem Provers,
- Verification for AI: how to prove AI algorithms (e.g. learning in neural networks) correct and secure,
- AI for Verification: applications of statistical machine learning in theorem proving,
- Induction and Coinduction, Recursion and Corecursion in logic and functional programming,
- Categorical Logic and Categorical Semantics of Computations.
Current Research grants (PI or CoI):
-
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.
-
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.
- 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.
- 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.
- 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.
Previous Research grants (as a PI):
- 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.
- 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.
- 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.
- 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.
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.
SICSA Industrial "Proof of Concept" grant
Machine-Learning for Industrial Theorem Proving, 2013-2014. Joint with Jonathan Heras.
-
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.
-
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:
- Spring 2019. SICSA grant for organising the first Scottish Summer School on Programming Languages and Verification.
- July 2017. Isaac Newton Institute (Cambridge) invited visitor at Big Proof research initiative.
- April 2013. SICSA workshop grant for ``Automated Reasoning Workshop" ARW'13, 11-12 April 2013, University of Dundee.
- April 2013. British Logic Colloquium workshop grant for ARW'13.
- June 2011. SICSA Workshop grant for organisation of the workshop``Scottish Theorem Proving",
University of Dundee, 12 June 2011.
-
July-August 2010, School of Computing, U. of Dundee. SICSA-funded grant ``Distinguished Academic Visitor",
for Dr John Power, Bath, UK.
- October 2009, School of Computer Science, University of St Andrews. Co-author of the SICSA-funded grant ``Distinguished Academic Visitor",
for Prof. Kai-Uwe Kuehnberger, Osnabrueck, Germany.
- 2005 -- 2007, Department of Mathemaics, University College Cork: Royal Society/Royal Irish Academy grant
``Category theory for natural models of computation'',
PIs: Dr John Power, Laboratory for Foundations of Computer Science, University of Edinburgh, UK, and Dr Anthony Seda, Department of Mathematics, University College Cork, Ireland.
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.