Validation and Verification (VALVE)

Introduction

In VALVE, we are interested in checking that programs (and designs) indeed do what we meant them to do. Generally speaking we are interested in testing programs, understanding them, and in proving that they are correct. Our work includes studying models that enable to better represent behavior of programs, creating techniques for the analysis of programs, and working on  new designs of programs that are built with validation in mind. Our work combines theoretical results and practical implementations. It relies on logic, formal methods, and computational structures.

Staff Members

Phd Students

  • Alexey Bakhirkin - combinations of static analysis and model checking (Nir Piterman, in collaboration with Microsoft Research Cambridge)
  • Basil Eljuse - automated test generation to explore non-functional properties of integrated circuits (Neil Walkinshaw, in collaboration with ARM)
  • Andrea Giugliano - formal methods applied to file systems  (Tom Ridge, in collaboration with Microsoft Research Cambridge)
  • John Whitington  - functional programming languages (Tom Ridge)
  • Yi Xiao - learning nominal automata (Emilio Tuosto and Alexander Kurz)

Overview

Topics

  • Formal verification for real-world systems: Formal verification using interactive and automated theorem provers is an established area with many successful applications (e.g., the CompCert compiler verification project). The aim of this current research is to apply formal methods to analyze existing systems (such as file systems), and to develop new systems (for example, usage of Formal Methods to prove the correctness of a new parsing technique). We are currently developing a new formally verified file system.  (Tom Ridge)
  • Choreography-based analysis: Models of choreography have recently received great attention as suitable abstractions of distributed coordination in communication-centric systems. The main objective of this research topic is to develop new verification and validation methods driven by choreography models.(Emilio Tuosto)
  • Nominal automata: Several research groups have developed different classes of nominal automata, that is finite state machines capable of dealing with languages on infinite alphabets. The main objectives of this research topic is to apply nominal automata for the modelling and analysis of resource-aware systems, namely systems that can allocate, communicate, and dispose resources. (Emilio Tuosto)
  • Executable Biology: Executable Biology uses computer artefacts as models of biological behavior and design and analysis principles that are usually used on software/hardware are applied to such models to gain better understanding of the biological system. Our main interest in executable biology is in developing reasoning and analysis techniques that are applicable to the type of artefacts that arise from constructing such executable models. (Nir Piterman)
  • Synthesis from Temporal Specifications: The idea behind this type of synthesis is to produce automatically reactive systems from high level specifications. More specifically, we consider specifications in temporal logic and produce a system that satisfies the specifications while being open to interaction with its environment. Our research in this field concentrates on the methods and methodologies that enable this kind of pursuit. (Nir Piterman)
  • Automata for reasoning about Probabilistic Systems: Automata provide a unifying approach for model checking, temporal logic, synthesis and abstraction on discrete systems. In this project we work on a concept of automata that can do the same for reasoning about probabilistic systems. We call our automata p-automata and the main research directions we are pursuing are applications to probabilistic temporal logic and abstraction of Markov chains.(Nir Piterman)
  • Automated test generation and assessment: The goal is to automatically generate inputs to a system for which the source code may not be accessible. We reason about test set completeness (i.e. their capacity to expose faulty behaviour) by adapting established techniques from the field of Machine Learning. (Neil Walkinshaw)
  • Software defect prediction: The goal of software defect prediction is to identify which modules in the source code of a software are more likely to contain defects. This task is usually performed before software testing, so that it can guide the allocation of testing resources towards concentrating more testing effort in the modules more likely to contain defects. In this way, testing cost-effectiveness can be increased. (Leandro Minku)

Industrial Projects

  • Project proposal: design, implement and verify a file system (Tom Ridge)
  • PREPAReD - Predicting, Preventing and Analysing Rail Delays, sponsored by DfT (Neil Walkinshaw and Emilio Tuosto).

Contact

Contact details for each staff member and most PhD students are available from their respective homeapages.

For general details please drop Nir an email.

Share this page: