LAIV Research and Projects

LAIV has a dedicated Githib page, for all the new projects by students and staff.

Neural Networks with Security Contracts

NCSC-funded research project SecCon-NN: Neural Networks with Security Contracts — towards lightweight, modular security for neural networks. Funded as part of NCSC “Security for AI” call.

LAIV Members involved: Komendantskaya, Kokke, Kienitz, with input from David Aspinall, University of Edinburgh

Verification of AI Planning languages

It is becoming increasingly important to verify safety and security of AI applications. While declarative languages (of the kind found in automated planners and model checkers) are traditionally used for verifying AI systems, a big challenge is to design methods that generate verified executable programs. A good example of such a “verification to implementation” cycle is given by AI planning languages like PDDL/STRIPS, where plans are found via a model search in a declarative language, but then interpreted or compiled into executable code in an imperative language. We show that this method can itself be verified. We present a formal framework and a prototype Agda implementation that represent PDDL plans as executable functions that inhabit types that are given by formulae describing planning problems. By exploiting the well-known Curry-Howard correspondence, type-checking then automatically ensures that the generated program corresponds precisely to the specification of the planning problem.

LAIV Members involved: Komendantskaya, Farka, Hill

Verification of Neural Networks

Neural Networks and Convolutional Neural Networks are no longer just a popular research topic, they have found their way into our everyday lives via a variety of tools and applications: from face recognition apps on our phones to autonomous driving features in our cars. But are they really reliable? In this project, we develop novel methods of verification of neural networks.

LAIV Members involved: Komendantskaya, Stewart, Duncan, Kienitz, MSc students

Coinduction and Coalgebra: semantics of nonterminating processes

Coinduction is a mathematical (and reasoning) principle allowing to express properties of nonterminating or concurrent processes, programs and systems. We are interested in using coinduction to analyse properties of nonterminating logic programs.

LAIV Members involved: Komendantskaya, Li, Farka.

Machine Learning for verification

Formal verification can be a laborious but also a repetitive task. Machine learning can be used to data mine the history of past verification efforts, in order to discover common proof heuristics and guide new proof development. Development of such methods is a subject of our ML4PG and ACL2ML projects.

LAIV Members involved: Komendantskaya, Hill.