Write a Blog >>
PLDI 2020
Mon 15 - Fri 19 June 2020
Alastair Reid

Registered user since Thu 16 Jan 2020

Name: Alastair Reid

Bio: Researcher at Google (UK) 2019-present

  • Rust verification tools
  • Formal verification of hypervisors

Researcher at Arm Ltd (UK) 2004-2019

  • Model checking processor pipelines (newest)
  • Formal architecture specifications
  • Wide SIMD instruction set
  • Pipeline parallelism
  • Software defined radio
  • Vectorising compilers (oldest)

Researcher at University of Utah (USA), 1998-2004

  • Component based / Library operating systems

Researcher at Yale University (USA), 1994-1998

  • Haskell foreign function interface
  • Functional Reactive Programming
  • Visual Tracking in Haskell
  • Haskell library/compiler development

Researcher at University of Glasgow (UK), 1988-1994

  • Formal specification and verification
  • GHC foreign function interface


  • Ph.D. Glasgow University, “Defining interfaces between hardware and software: Quality and performance”
  • M.Sc. Glasgow University, “A precise semantics for Ultraloose Specifications”
  • B.Sc. University of Strathclyde.

Country: United Kingdom

Affiliation: Google Research

Personal website: https://alastairreid.github.io/

Research interests: formal verification, security, functional languages, computer architecture


REMS-DeepSpec 2020Author of Sail: ISA semantics, symbolic execution, and axiomatic concurrency for ARMv8-A and RISC-V within the REMS-DeepSpec 2020-track
Show activities from other conferences

PLDI 2020-profile
View general profile