Many congratulations to Dr Daniel Kienitz, who successfully passed his viva exam on “The Influence of Geometric Properties of Data Distributions on Artificial Neural Networks” on the 26th of October 2023!
Welcome to new PhD students
Huge welcome to our new PhD students, Ben Coke, who will be working on Verification of Neural Networks in Engineering Applications (as part of ICASE Studentship led by SLB Cambridge) and Colin Kessler, who will be working in the Edinburgh Center for Robotics on Safe Design of Airborne Autonomous Systems with Neural Network Components.
Success of MSc students using Vehicle
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/
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: https://vehicle-lang.github.io/tutorial/
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 ek19@hw.ac.uk
Congratulations to Natalia Slusarz
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/
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!
Omri Isac, Visitor from the Marabou team
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. 🙂
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 https://laiv.uk/laiv-seminars/ Join us!
CPP’23 paper accepted!
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.