Vehicle Tutorial

Many LAIV members are involved in the design and testing of the Vehicle specification language (for verifying neural networks). This Summer and Autumn, the team is giving a series of tutorials on Vehicle, at FOMLAS’23 in Paris, VETSS Summer School in Surrey and ICFP Tutorial fest in Seattle. All Vehicle tutorial materials are available here:

PhD post available:

Neural Network Verification in Vehicle in the Industrial setting. The studentship is funded by SLB, and will include internships in SLB Cambridge. Interested candidates should email

Congratulations, Dr Alasdair Hill!

LAIV PhD Alasdair Hill has successfully defended his dissertation, entitled “Planning Problems as Types, Plans as Programs: A Dependent Types Infrastructure for Verification and Reasoning about Automated Plans in Agda” , examiners Andreas Abel, Chalmers and Manuel Maarek, HWU. Conratualtions, Ali!

LAIV Seminars restarting this week!

Happy New Year! LAIV Seminars are restarting this week with a talk by Henning Basold on “Guarded Recursion for Coinductive, Higher-Order Stochastic Systems”. Full program of talks is on Join us!

New LAIV PhD students

We are happy to welcome two new PhD students this Autumn: Remi Desmartin, who will work with supervisors Komendantskaya, Stark and Passmore (from on neural network libraries in Imandra and Aina Centelles Tarres, who will work with supervisors Gabbay and Komendantskaya on nominal logic for neural network verification. Remi and Aina, have a great and productive time during your PhD studies!

ACCV success of Daniel Kienitz

LAIV PhD student, Daniel Kienitz, has just had his paper accepted at the Asian Conference on Computer Vision (ACCV 2022): D. Kienitz, E. Komendantskaya and M. Lones.  Comparing Complexities of Decision Boundaries for Robust Training: A Universal Approach. Many congratulations, Daniel!