On the Architecture of a (Verifying) Compiler

David Pearce explores the architecture of a verifying compiler for the Whiley programming language, focusing on incremental compilation and static analysis.

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.