Write a Blog >>
Sun 22 - Fri 27 October 2017 Vancouver, Canada
Thu 26 Oct 2017 16:37 - 17:00 at Regency C - Verification in Practice Chair(s): Davide Ancona

Software and hardware are increasingly being formally verified against
specifications, but how can we verify the specifications themselves? This paper
explores what it means to formally verify a specification. We solve three
challenges: (1) How to create a secondary, higher-level specification that can
be effectively reviewed by processor designers who are not experts in formal
verification; (2) How to avoid common-mode failures between the specifications;
and (3) How to automatically verify the two specifications against each other.

One of the most important specifications for software verification is the
processor specification since it defines the behaviour of machine code and of
hardware protection features used by operating systems. We demonstrate our
approach on ARM's v8-M Processor Specification, which is intended to improve
the security of Internet of Things devices. Thus, we focus on establishing the
security guarantees the architecture is intended to provide. Despite the fact
that the ARM v8-M specification had previously been extensively tested, we
found twelve bugs (including two security bugs) that have all been fixed by

Researcher at Arm Ltd (UK) since 2004

  • 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 operating system kernels

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

Thu 26 Oct
Times are displayed in time zone: (GMT-07:00) Tijuana, Baja California change

15:30 - 17:00: Verification in PracticeOOPSLA at Regency C
Chair(s): Davide AnconaUniversity of Genova
15:30 - 15:52
Magnus MadsenUniversity of Waterloo, Ondřej LhotákUniversity of Waterloo, Canada, Frank TipNortheastern University
15:52 - 16:15
David SwaseyMPI-SWS, Germany, Deepak GargMax Planck Institute for Software Systems, Derek DreyerMPI-SWS
16:15 - 16:37
William ManskyPrinceton University, Andrew AppelPrinceton, Aleksey NoginHRL Laboratories, LLC
16:37 - 17:00