Research

Research Outline

I am interested in automated techniques for helping developers to write reliable software that runs efficiently on modern hardware.

Formal verification techniques for multicore software. I am especially interested in lightweight, automatic formal verification techniques, capable of operating directly on source code, that can be implemented as efficient tools to be used in day-to-day software development.

My current research in this area is on static data-race analysis for multicore programs, based on:

• symbolic model checking
• k-induction
• abstract interpretation
• separation logic

Other verification-related interests include predicate abstraction for concurrent programs, and symmetry reduction techniques for model checking.

Software performance optimization for multicore processors. To take advantage of modern multicore processors, we need suitable abstractions to allow programmers to write high-level, portable programs, from which efficient parallel code can be generated. I got interested in this area while working as a Research Engineer at Codeplay Software Ltd., and continue to collaborate with Codeplay on this topic, as well as with the group of Prof. Paul Kelly at Imperial College London.

Selected Papers

List of all my papers.

• NEW! Safe Asynchronous Memory Operations (ASE'11)
• NEW! Software Verification Using k-Induction (SAS'11)
• Symmetry-Aware Predicate Abstraction for Shared Variable Concurrent Programs (CAV'11)
• Automatic Analysis of Scratch-pad Memory Code for Heterogeneous Multicore Processors (TACAS'10)
• Offload - Automating Code Migration to Heterogeneous Multicore Systems (HiPEAC'10)
• On the Constructive Orbit Problem (Annals of Mathematics and Artificial Intelligence)
  This is an extended version of a paper at FM'06
• Language-level Symmetry Reduction for Probabilistic Model Checking (QEST'09)
• Deriving Efficient Data Movement From Decoupled Access/Execute Specifications (HiPEAC'09)
• Automatic Symmetry Detection for Promela (Journal of Automated Reasoning)
  This is an extended version of a paper at FM'05
• Compile-time and Run-time Issues in an Auto-parallelisation System for the Cell BE Processor (HPPC'08)
• Symmetry in Temporal Logic Model Checking (ACM Computing Surveys)

Tools

• SCRATCH - automatic DMA race analysis for the Cell BE processor
• Offload C++ - a framework for offloading portions of C++ applications to run across the SPE cores of the Cell BE processor. Designed and developed by Codeplay Software Ltd. (my former employer)
• TopSPIN - an automatic symmetry reduction package for the SPIN model checker
• Etch - an enhanced type checker for Promela. Etch can statically detect type errors in Promela specifications that are missed by the SPIN tool
• GRIP - a symmetry reduction tool for the PRISM model checker