Category: Non classé

Many congratulations to Ben Coke and Jeonghyeon Lee, who got A marks for MSc dissertations completed with Vehicle. Their contributions are also a part of the Vehicle tutorial: https://vehicle-lang.github.io/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: https://vehicle-lang.github.io/tutorial/

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 ek19@hw.ac.uk

Many congratulations to Natalia Slusarz and all supervisors

for having the paper: Natalia Ślusarz, Ekaterina Komendantskaya, Matthew L. Daggitt, Robert Stewart, Kathrin Stark Logic of Differentiable Logics: Towards a Uniform Semantics of DL

accepted at LPAR’23: https://easychair.org/smart-program/LPAR2023/

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!

This week and for 2 more weeks, we are hosting Omri Isac, a visitor from the Marabou team run by Guy Katz at HUJI . Check Omri’s talk at LAIV seminar pages, and his presentation at SPLS on the 8th of March. 🙂

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 https://laiv.uk/laiv-seminars/ Join us!

Many congratualtions to the team for having a paper accepted at CPP’23, Certified Proofs and programs: 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.

Katya and Natalia are attending the Mathematical Components Winter School and workshop in INRIA Sophia Antipolis, France this week.

We are happy to welcome two new PhD students this Autumn: Remi Desmartin, who will work with supervisors Komendantskaya, Stark and Passmore (from Imandra.ai) 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!