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.
Our team is giving tutorials about Vehicle at FOMLAS'23 in Paris, VETSS Summer School'23 in Surrey and ICFP'23 in Seattle.
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.
2023 Running Grants:
Research project AISEC:
AI Secure and Explainable by Construction, is now running on full speed.
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 Invited talks and tutorials:
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, 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
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 PC membership:
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
Unity of Logic and Computation, 24-28 July 2023, Batumi, Georgia
HCVS2023 , the 10th workshop on Horn Clauses for Verification and Synthesis 2023.
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 (TYPES 2023)
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.