LAIV Publications

2024 Conference Publications

• Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Ślusarz, Kathrin Stark. Taming Differentiable Logics with Coq Formalisation. Interactive Theorem Proving (ITP) Tbilisi, Georgia, September 2024.
• 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.
• Parth Padalkar, Natalia Slusarz, Gopal Gupta, Ekaterina Komendantskaya, A Neurosymbolic Framework for Bias Correction in Convolutional Neural Networks. International Conference on Logic Programming, ICLP 2024. Journal Proceedings in the Journal of Theory and Practice of Logic Programming.

2023 Conference Publications

• Matthew L. Daggitt, Wen Kokke, Ekaterina Komendantskaya, Robert Atkey, Luca Arnaboldi, Natalia Slusarz, Marco Casadio, Ben Coke, and Jeonghyeon Lee. The Vehicle Tutorial: Neural Network Verification with Vehicle. The 6th Workshop on Formal Methods for ML-Enabled Autonomous Systems (FoMLAS’23).
• Natalia Slusarz, Ekaterina Komendantskaya, Matthew L. Daggitt, Robert J. Stewart, Kathrin Stark: Logic of Differentiable Logics: Towards a Uniform Semantics of DL. LPAR’2023, 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning.
• Matthew L. Daggitt, Robert Atkey, Wen Kokke, Ekaterina Komandantskaya, Luca Arnaboldi Compiling higher-order specifications to SMT solvers: how to deal with rejection constructively. Certified Proofs and Programs. CPP’23. Boston, USA, 16-17 January 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
• Marco Casadio, Luca Arnaboldi, Matthew L. Daggitt, Omri Isac, Tanvi Dinkar, Daniel Kienitz, Verena Rieser, Ekaterina Komendantskaya: ANTONIO: Towards a Systematic Method of Generating NLP Benchmarks for Verification. FOMLAS’2023 — The 6th Workshop on Formal Methods for ML-Enabled Autonomous Systems

2023 PhD and MSc Dissertations

Daniel Kienitz: “The Influence of Geometric Properties of Data Distributions on Artificial Neural Networks”. PhD dissertation, Heriot-Watt University, 2023.

Alasdair Hill “Planning Problems as Types, Plans as Programs: A Dependent Types Infrastructure for Verification and Reasoning about Automated Plans in Agda” PhD Dissertation, Heriot-Watt University, 2023.

Ben Coke: MSc dissertation topic: Neural Network Verification with Vehicle. Supervisors: E.Komendantskaya

Jeonghyeon Lee: MSc dissertation topic: Neural Network Explainability meets Verification (in Vehicle). Supervisors: E.Komendantskaya

2022 Conference Publications:

• D. Kienitz, E. Komendantskaya and M. Lones. The Effect of Manifold Entanglement and Intrinsic Dimensionality on Learning. Thirty-Sixth AAAI Conference on Artificial Intelligence (AAAI22).
• D. Kienitz, E. Komendantskaya and M. Lones.  Comparing Complexities of Decision Boundaries for Robust Training: A Universal Approach. Asian Conference on Computer Vision (ACCV 2022).
• 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).
• R. Desmartin, G. Passmore E. Komendantskaya and M. Daggitt: CheckINN: Wide Range Neural Network Verification in Imandra. 24th International Symposium on Principles and Practice of Declarative Programming PPDP’22.
• M. Daggitt, W. Kokke, R. Atkey, L. Arnaboldi and E. Komendantskaya: Vehicle: A High-Level Language for Embedding Logical Specifications in Neural Networks. The 5th Workshop on Formal Methods for ML-Enabled Autonomous Systems (FoMLAS’22).
• N. Slusarz, E. Komendantskaya, M. Daggitt and R. Stewart: Differentiable Logics for Neural Network Verification. The 5th Workshop on Formal Methods for ML-Enabled Autonomous Systems (FoMLAS’22).
• M. Casadio, E. Komendantskaya, V. Rieser, M. Daggitt, D. Kienitz, L. Arnaboldi and W. Kokke: Why Robust Natural Language Understanding is a Challenge. The 5th Workshop on Formal Methods for ML-Enabled Autonomous Systems (FoMLAS’22).
• R. Desmartin, G. Passmore and E. Komendantskaya: Neural Networks in Imandra: Matrix Representation as a Verification Choice. The 5th Workshop on Formal Methods for ML-Enabled Autonomous Systems (FoMLAS’22).
• Taryn Scharf, Chris Kirkland, Matthew Daggitt, Milo Barham, Vladimir Puzyrev. AnalyZr: A Python application for zircon grain image segmentation and shape analysis Computers & Geosciences 2022

2022 MSc dissertations:

Henri-Louis Boisvert: Evaluating the Performance of Different Reinforcement Learning Methods for Autonomous Racing MSc Dissertation at Heriot-Watt University, Best Msc Dissertation award 2022. Supervisors: L. Arnaboldi and E.Komendantskaya

Youssef Bonnaire: Improving and Generating LiDAR Data in Adverse Weather using GANs. MSc Dissertation at Heriot-Watt University. Supervisors: M.Casadio and E.Komendantskaya

Assya Chiguer: Explainable AI and Property-Driven Training. MSc Dissertation at Heriot-Watt University. Supervisors: E.Komendantskaya, N.Slusarz, M.Casadio

Sinead Donnelly: Formal Verification of an Autonomous Car Controller. MSc Dissertation at Heriot-Watt University. Supervisors: M.Daggitt and E.Komendantskaya

Haoran Hong: Autonomous Racing: a Real-Time Dynamic Path-Planning Approach Based on Racing Theory. MSc Dissertation at Heriot-Watt University. Supervisors: M.Daggitt and E.Komendantskaya

Samuel Moses: Visual Odometry of Autonomous Cars using Event Camera. MSc Dissertation at Heriot-Watt University. Supervisors: E.Komendantskaya, Y.Lin

2021 Conference Publications:

• Alasdair Hill, Ekaterina Komendantskaya, Matthew L. Daggitt, Ronald P. A. Petrick. Actions You Can Handle: Dependent Types for AI Plans. Workshop on Type-driven Development’ 21, at ICFP’21, 2021.
• Kirsty Duncan, Robert Stewart and Ekaterina Komendantskaya.  Logically Constrained Pruning Towards Robust Neural Networks. FOMLAS’21, Workshop on Formal Methods for ML-Enabled Autonomous Systems, at CAV’21.

2021 BSc and MSc dissertations:

Natalia Slusarz: Mathematical Properties of Neural Networks Trained on Artificial Data Sets. BSc Dissertation at Heriot-Watt University, 2021. Supervisors: E.Komendantskaya and D.Kienitz

Remi Desmartin: Neural Network Verification with Imandra. MSc Dissertation at Heriot-Watt University, 2021. Best Dissertation award. Supervisors: E.Komendantskaya and M.Daggitt

Dan Green: Understanding the Role of Machine Learning in Signed Language Recognition. Supervisors: E.Komendantskaya and M.Daggitt

Michael Pidgeon: Building Trust in Explanations of Machine Learning tools. MSc Dissertation at Heriot-Watt University, 2021. Supervisors: E.Komendantskaya and M.Daggitt

2020 Conference Publications:

• Wen Kokke, Ekaterina Komendantskaya, Daniel Kienitz, Bob Atkey and David Aspinall. Neural Networks, Secure by Construction: An Exploration of Refinement Types. Accepted for Publication at APLAS’20, The 18th Asian Symposium on Programming Languages and Systems.
• Alasdair Hill, Ekaterina Komendantskaya and Ron Petrick. Proof-Carrying Plans: a Resource Logic for AI Planning PPDP’20, the 22nd International Symposium on Principles and Practice of Declarative Programming.
• Ekaterina Komendantskaya, Dmitry Rozplokhas and Henning Basold. The New Normal: We Cannot Eliminate Cuts in Coinductive Sequent Calculi, But We Can Explore Them. ICLP’20, the 36th International Conference on Logic Programming.
• Wen Kokke, Ekaterina Komendantskaya, Daniel Kienitz and David Aspinall. Robustness as a Refinement Type: Verifying Neural Networks in Liquid Haskell and F*. Accepted at ETAPS Workshop LiVe’20: 4th Workshop on Learning in Verification, 25 April 2020, Dublin, Ireland.
• Kirsty Duncan, Ekaterina Komendantskaya, Robert Sewart, Michael Lones Relative Robustness of Quantized Neural Networks Against Adversarial Attacks, accepted to be published and presented at the International Joint Conference on Neural Networks, IJCNN’20, part of the world congress on computational intelligence: https://wcci2020.org/ 19-24 July 2020, Glasgow, Scotland.
• Pascal Bacchus, Robert Stewart and Ekaterina Komendantskaya. Accuracy, Training Time and Hardware Efficiency Trade-Offs for Quantised Neural Networks on FPGAs. 16th International Symposium on Applied Reconfigurable Computing (ARC2020), 1-3 April   Toledo, Spain.

2020 MSc and PhD Dissertations:

• Alexandre Cardaillac. Explainable AI: Methods to Evaluate Machine Learning Models. MSc Dissertation. 2020. Supervisor: E.Komendantskaya.
• Marco Casadio. Generative Against Logical Training against Adversarial Attacks. MSc Dissertation. 2020. Supervisor: E.Komendantskaya.
• Hugo Cousin. High-performance Data Analysis for Social Networks Using Rust. MSc Dissertation. 2020. Supervisor: H.-W. Loidl.
• Fraser Garrow. Artificial Neural Network Genetic Improvement for Accurate and Robust Image Classification. MSc Dissertation. 2020. Supervisor: M.Lones.
• Dorian Gouzou. Repelling Dual-Swarm Particle Optimisation with Maximisation search. MSc Dissertation. 2020. Supervisor: M.Lones.
• Vincent Larcher. Generation of Adversarial Attacks on Computer Vision Models using Reinforcement Learning. MSc Dissertation. 2020. Supervisor: E.Komendantskaya.
• Bartosz Schatton. Informed Adversarial Examples with Explainable AI and Metaheuristics in Medical Imaging. MSc Dissertation. 2020. Supervisor: E.Komendantskaya.
• Frantisek Farka. Proof-Relevant Resolution: The Foundations of Constructive Proof Automation. PhD Dissertation. 2020. Supervisor: E.Komendantskaya.

2019 Conference papers:

• C.Schwaab, E.Komendantskaya, A.Hill, F.Farka, J.Wells, R.Petrick, K.Hammond. Proof-Carrying Plans. PADL 2019 (21st International Symposium on Practical Aspects of Declarative Languages), 14-15 January 2019, Cascais/Lisbon, Portugal.
• 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, R. Stewart, K. Duncan, D. Kienitz, P. Le Hen, P. Bacchus. Neural Network Verification for the Masses (of AI graduates). Experience report, June 2019

2019 MSc and PhD Dissertations:

• P. Bacchus. Performance Metrics for Approximate Deep Learning on Programmable Hardware. MSc Thesis, Heriot-Watt University, 2019. Supervisor: R. Stewart.
• P. Le Hen. Adversarial Attacks on Neural Networks in Image Processing. MSc Thesis, Heriot-Watt University, 2019. Supervisor: E.Komendantskaya.
• D. Kienitz. Robustness of Neural Networks: Understanding the Nature of Adversarial Examples. MSc Thesis, Heriot-Watt University, 2019. Supervisor: E.Komendantskaya.
• Y.Li. A Proof-Theoretic Approach to Coinduction in Horn Clause Logic” . PhD Thesis, Heriot-Watt University, 2019. Supervisor: E.Komendantskaya and M.Lawson.