On the Architecture of a (Verifying) Compiler

David Pearce

School of Engineering and Computer Science
Victoria University of Wellington

Abstract:

Modern programming languages and tools pose increasing challenges for
the compiler designer. For example, they are typically expected to
support incremental compilation, multiple backend targets, package
management, static analysis, sophisticated type systems and much more.
On top of this, a verifying compiler must generate verification
conditions and provide confidence in the overall correctness of
compilation and verification.

In this talk, I will explore the architecture of a verifying compiler
for the Whiley programming language. This language certainly has its
share of unusual features (such as structural types and flow typing)!
And yet, at the same time, it is quite representative of a modern
imperative and statically typed language. As such, many of the
approaches developed (e.g. for incremental compilation) have
applicability to a wide range of languages.

Bio:

David (@whileydave) graduated with a PhD from Imperial College London in
2005, and took up a lecturer position at Victoria University of
Wellington, NZ. David’s PhD thesis was on efficient algorithms for
pointer analysis of C, and his techniques have since been incorporated
into GCC . His interests are in programming languages, compilers and
static analysis.

Since 2009, he has been developing the Whiley Programming Language
(whiley.org) which is designed specifically to simplify program
verification. David has previously interned at Bell Labs, New Jersey,
where he worked on compilers for FPG As; and also at IBM Hursely, UK,
where he worked with the AspectJ development team on profiling systems.