Analysis and Verification

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.

Play video

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

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

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

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

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.

Groups

Centres

Research Institute in Verified Trustworthy Software Systems

Academics

Dr Cristian Cadar

Personal details
Dr Cristian Cadar Professor in Software Reliability
Send email+44 (0)20 7594 8244

Research interests

Software Engineering, Computer Systems and Software Security, with a focus on building practical techniques for improving the reliability and security of software systems.

Location

435, Huxley Building
Dr Alastair Donaldson

Personal details
Dr Alastair Donaldson Professor
Send email+44 (0)20 7594 8266

Research interests

Formal verification techniques for multicore software. Software performance optimization for multicore processors.

Location

422, Huxley Building
Prof. Sophia Drossopoulou

Personal details
Prof. Sophia Drossopoulou Professor of Programming Languages
Send email+44 (0)20 7594 8368

Research interests

Object Capability Policies, Concurrent Programming, Program Verification, Characterization of Program Evolution and Theorem Proving.

Location

559, Huxley Building
Prof. Susan Eisenbach

Personal details
Prof. Susan Eisenbach Emeritus Professor
Send email+44 (0)20 7594 8264

Research interests

Programming Languages, Concurrency and Testing.

Location

569, Huxley Building
Dr Antonio Filieri

Personal details
Dr Antonio Filieri Lecturer
Send email+44 (0)20 7594 9478

Research interests

Exact and approximate methods for probabilistic software analysis and probabilistic programming, Control Theory for Software Engineering, and Runtime-efficient and incremental verification of quantitative and functional software properties.

Location

572, Huxley Building
Prof. Philippa Gardner

Personal details
Prof. Philippa Gardner Professor of Theoretical Computer Science
Send email+44 (0)20 7594 8292

Research interests

JavaScript, Concurrency and Resource Reasoning.

Location

453, Huxley Building
Prof. Michael Huth

Personal details
Prof. Michael Huth Professor of Computer Science and Head of Department
Send email+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

Personal details
Dr Ben Livshits Reader
Send email

Research interests

Security, Privacy, Program Analysis, Compilers, Software Engineering and Crowdsourcing.

Location

569, Huxley Building
Prof. Alessio Lomuscio

Personal details
Prof. Alessio Lomuscio Professor of Safe Artificial Intelligence
Send email+ 44 (0)20 7594 8414

Research interests

Logic-Based Specification and Verification of Autonomous Systems.

Location

504, Huxley Building
Dr Sergio Maffeis

Personal details
Dr Sergio Maffeis Senior Lecturer
Send email+44 (0)20 7594 8390

Research interests

Computer Security, Web Programming and Process Calculi.

Location

441, Huxley Building
Dr. Azalea Raad

Personal details
Dr. Azalea Raad Lecturer
Send email

Location

Huxley Building
Dr Herbert Wiklicky

Personal details
Dr Herbert Wiklicky Reader in Computer Science
Send email+44 (0)20 7594 8206

Research interests

Program Analysis, semantics of programming languages, Probabilistic Models, Program Synthesis, semantics in Computer Security and Quantum Computation.

Location

424, Huxley Building
Prof. Nobuko Yoshida

Personal details
Prof. Nobuko Yoshida Professor of Computing
Send email+44 (0)20 7594 8240

Research interests

Theoretical Computer Science.

Location

556, Huxley Building