Analysis and Verification
We face a fundamental problem: computer systems are critical to modern society but traditional non-mathematical computer engineering techiques, 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 developements 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
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
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.
Research groups and centres
Academics
Academics
-
Dr Cristian Cadar
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
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 LanguagesSend 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
Research interests
Programming Languages, Concurrency and Testing.
Location
569, Huxley Building
-
Dr Antonio Filieri
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
421, Huxley Building
-
Prof. Philippa Gardner
Personal details
Prof. Philippa Gardner Professor of Theoretical Computer ScienceSend email+44 (0)20 7594 8292
Research interests
JavaScript, Concurrency and Resource Reasoning.
Location
453, Huxley Building
-
Prof. Michael Huth
Research interests
Trusted Computing, Access Control, Formal Methods, Insider Threats, Model-Driven Security, Risk Analysis.
Location
364, ACE Extension
-
Dr Ben Livshits
Research interests
Security, Privacy, Program Analysis, Compilers, Software Engineering and Crowdsourcing.
Location
569, Huxley Building
-
Prof. Alessio Lomuscio
Personal details
Prof. Alessio Lomuscio Professor in Logic for Multiagent SystemsSend email+ 44 (0)20 7594 8414
Research interests
Logic-Based Specification and Verification of Autonomous Systems.
Location
504, Huxley Building
-
Dr Sergio Maffeis
Research interests
Computer Security, Web Programming and Process Calculi.
Location
441, Huxley Building
-
Dr Herbert Wiklicky
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
Research interests
Theoretical Computer Science.
Location
556, Huxley Building