Designing a verifying compiler: Lessons learned from developing Whiley

• We reflect on our experiences verifying software with the Whiley verifying compiler.
• We identify a number of patterns for resolving common verification problems.
• We report on three case studies illustrating software verification with Whiley.

An ongoing challenge for computer science is the development of a tool which automatically verifies programs meet their specifications, and are free from runtime errors such as divide-by-zero, array out-of-bounds and null dereferences. Several impressive systems have been developed to this end, such as ESC/Java and Spec#, which build on existing programming languages (e.g., Java, C#). We have been developing a programming language from scratch to simplify verification, called Whiley, and an accompanying verifying compiler. In this paper, we present a technical overview of the verifying compiler and document the numerous design decisions made. Indeed, many of our decisions reflect those of similar tools. However, they have often been ignored in the literature and/or spread thinly throughout. In doing this, we hope to provide a useful resource for those building verifying compilers.