We face a fundamental problem: computer systems are critical to modern society but traditional non-mathematical computer engineering techniques, such as informal prose specification and ad-hoc testing, cannot make them safe, reliable and secure. The only solution is to bring a mathematically rigorous, scientific method to the specification, testing and verification of the complex computer infrastructure on which society depends.

The Verification theme comprises academics unified by a common interest in symbolic analysis at scale, at the forefront of research developments in fundamental theories and industrial-strength tools, targeting real-world applications ranging from multi-core systems, programming languages, autonomous vehicles and web services. Our specialist research uses techniques such as symbolic testing, program logics, type theories, model checking and process algebras.

Related videos

Specification and verification of x86 machine-level code

We are using theorem-proving techniques to model and analyze x86 software for the purpose of increasing the accuracy and reliability of x86-based products. We have developed an ISA-level x86 emulator in the ACL2 logic; this emulator serves as a precise specification for x86 software.

Specification and verification of x86 machine-level code

Specification and verification of x86 machine-level code

We are using theorem-proving techniques to model and analyze x86 software

We are using theorem-proving techniques to model and analyze x86 software for the purpose of increasing the accuracy and reliability of x86-based products. We have developed an ISA-level x86 emulator in the ACL2 logic; this emulator serves as a precise specification for x86 software.

GPUVerify: Introduction and overview

GPUVerify: Introduction and overview

The video demonstrates GPUVerify in action on some practical examples

In this video, Alastair Donaldson provides an overview of GPUVerify, which is a tool for analysing OpenCL and CUDA kernels to check for data races and barrier divergence. The video demonstrates GPUVerify in action on some practical examples.

GPUVerify: Verification method

GPUVerify: Verification method

Alastair Donaldson explains how the technique works behind the hood

In this second video about GPUVerify, Alastair Donaldson explains about GPUVerify, how the technique works behind the hood, showing how data race analysis for a massively parallel kernel is reduced to analysis of a sequential program.

GPUVerify: Predicated execution and invariant inference

GPUVerify: Predicated execution and invariant inference

Alastair Donaldson covers two topics: the lock-step predicated execution technique and looping code

In the final video about GPUVerify, Alastair Donaldson covers two advanced topics: the lock-step predicated execution technique that the tool uses to handle conditional and looping code, and the manner by which loop invariants are automatically inferred using the Houdini algorithm.

Events

PhD students, RAs, and faculty whose work is related to the Programming Languages or Analysis & Verification themes are invited to take part in a regular get together for the theme

 

Academics

Academics

  • Dr Cristian Cadar

    Dr Cristian Cadar

    Personal details

    Dr Cristian Cadar Professor in Software Reliability

    +44 (0)20 7594 8244

    Research interests

    Software engineering, computer systems, software security, practical techniques for improving software reliability and security.

    Location

    435, Huxley Building

  • Prof Alastair Donaldson

    Dr Alastair Donaldson

    Personal details

    Prof Alastair Donaldson Professor

    +44 (0)20 7594 8266

    Research interests

    Formal verification for multicore software, software performance optimization.

    Location

    422, Huxley Building

  • Prof. Sophia Drossopoulou

    Prof. Sophia Drossopoulou

    Personal details

    Prof. Sophia Drossopoulou Professor of Programming Languages

    +44 (0)20 7594 8368

    Research interests

    Concurrent programming, program verification, characterization of program evolution, theorem proving.

    Location

    559, Huxley Building

  • Prof. Susan Eisenbach

    Prof. Susan Eisenbach

    Personal details

    Prof. Susan Eisenbach Emeritus Professor

    +44 (0)20 7594 8264

    Research interests

    Programming Languages, Concurrency and Testing.

    Location

    569, Huxley Building

  • Dr Antonio Filieri

    Dr Antonio Filieri

    Personal details

    Dr Antonio Filieri Senior Lecturer

    +44 (0)20 7594 9478

    Research interests

    Probabilistic software analysis, probabilistic programming, control theory for software engineering, runtime and incremental verification, quantitative and functional software properties.

    Location

    572, Huxley Building

  • Prof. Philippa Gardner

    Prof. Philippa Gardner

    Personal details

    Prof. Philippa Gardner Professor of Theoretical Computer Science

    +44 (0)20 7594 8292

    Research interests

    Programming languages, program analysis and verification, concurrency and resource reasoning.

    Location

    453, Huxley Building

  • Prof. Michael Huth

    Prof. Michael Huth

    Personal details

    Prof. Michael Huth Professor of Computer Science and Head of Department

    +44 (0)20 7594 8355

    Research interests

    Trusted computing, access control, formal methods, insider threats, model-driven security, risk analysis.

    Location

    364, ACE Extension

  • Dr Ben Livshits

    Dr Ben Livshits

    Personal details

    Dr Ben Livshits Reader

    Research interests

    Security, privacy, program analysis, compilers, software engineering and crowd-sourcing.

    Location

    569, Huxley Building

  • Prof. Alessio Lomuscio

    Prof. Alessio Lomuscio

    Personal details

    Prof. Alessio Lomuscio Professor of Safe Artificial Intelligence

    + 44 (0)20 7594 8414

    Research interests

    Logic-based specification, verification of autonomous systems.

    Location

    I-X, Translation and Innovation Hub (I-HUB), White City Campus

  • Dr Sergio Maffeis

    Dr Sergio Maffeis

    Personal details

    Dr Sergio Maffeis Senior Lecturer

    +44 (0)20 7594 8390

    Research interests

    Software security; network and web security; applications of machine learning to security; security of machine learning; formal methods.

    Location

    441, Huxley Building

  • Dr. Azalea Raad

    Dr. Azalea Raad

    Personal details

    Dr. Azalea Raad Lecturer

    Location

    Huxley Building

  • Dr Herbert Wiklicky

    Dr Herbert Wiklicky

    Personal details

    Dr Herbert Wiklicky Reader in Computer Science

    +44 (0)20 7594 8206

    Research interests

    Program analysis, programming languages, semantics, probabilistic models, program synthesis, semantics in computer security, quantum computation.

    Location

    424, Huxley Building