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.
Mathematical Components Winter School
Katya and Natalia are attending the Mathematical Components Winter School and workshop in INRIA Sophia Antipolis, France this week.
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 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!
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!
LAIV MSc student success
- MSc dissertation marks have been released, and MSc students supervised by the LAIV team: Youssef, Henri-Louis, Assya, Samuel, Sinead, Haoran, all got excellent marks (one B and five As). Many congratulations to the students, but also their supervisors: Luca, Matthew, Marco, Natalia, Yuhui! Well done all. If curious to see the final titles and supervisory teams, check them here.
- in addition, Henri-Louis Boisvert got a prize for the best MSc dissertation award for his thesis “Evaluating the Performance of Different Reinforcement Learning Methods for Autonomous Racing“. Many congratulations Henri-Louis and Luca (the main supervisor)!
We are starting a new Seminar season
LAIV/DSG seminars are restarting this week, with Remi’s talk on neural net verification in Imandra. Join us online or F2F!
PhD and postdoc positions at LAIV
The Lab for AI and Verification is looking to fill one PhD post and one postdoctoral post. We are looking for candidates with solid knowledge of Theorem Proving and/or Functional/Logic programming, and enthusiasm to apply this knowledge in the domain of Artificial Intelligence.
The PhD post is for 4 years, starting in October 2022. It covers full stipend and PhD fees and is sponsored by the UKRI (ukri.org) and Schlumberger Cambridge (slb.com). The company will provide additional training and support during the PhD studies. This post needs to be filled in as soon as possible.
We are also looking to employ a postdoctoral researcher for a 6-12 months project to formalise Criminal law in the Functional Language Catala. Formalising criminal law for autonomous cars is of particular interest. This project will be in collaboration with Jonathan Protzenko, Microsoft Research and the School of Law, Edinburgh University. This project has a flexible starting date.
Please direct all queries to Ekaterina Komendantskaya (ek19@hw.ac.uk)