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.
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.
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.
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
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
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):
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.
