Daniel's Blog

Implementing and Verifying "Static Program Analysis" in Agda

In this series, I attempt to formalize the first few chapters of [Static Program Analysis](https://cs.au.dk/~amoeller/spa/) in Agda. The goal is to have a formally verified, yet executable, static analyzer for a simple language.

• Intro

  860 words, about 5 minutes to read.

  Some years ago, when the Programming Languages research group at Oregon State University was discussing what to read, the Static Program Analysis lecture notes came up. The group …

• Lattices

  4965 words, about 24 minutes to read.

  This is the first post in a series on static program analysis in Agda. See the introduction for a little bit more context.

• Combining Lattices

  5430 words, about 26 minutes to read.

  In the previous post, I wrote about how lattices arise when tracking, comparing and combining static information about programs. I then showed two simple lattices: the natural …

• Lattices of Finite Height

  7172 words, about 34 minutes to read.

  In the previous post, I introduced the class of finite-height lattices: lattices where chains made from elements and the less-than operator < can only be so long. As a first …

• The Fixed-Point Algorithm

  2308 words, about 11 minutes to read.

  In the preivous post we looked at lattices of finite height, which are a crucial ingredient to our static analyses. In this post, I will describe the specific algorithm that makes …

• Our Programming Language

  3794 words, about 18 minutes to read.

  In the previous several posts, I’ve formalized the notion of lattices, which are an essential ingredient to formalizing the analyses in Anders Møller’s lecture notes. …

• Control Flow Graphs

  3660 words, about 18 minutes to read.

  In the previous section, I’ve given a formal definition of the programming language that I’ve been trying to analyze. This formal definition serves as the “ground …

• Connecting Semantics and Control Flow Graphs

  4192 words, about 20 minutes to read.

  In the previous two posts, I covered two ways of looking at programs in my little toy language: In part 5, I covered the formal semantics of the programming language. These are …

• Forward Analysis

  5332 words, about 26 minutes to read.

  In the previous post, I showed that the Control Flow graphs we built of our programs match how they are really executed. This means that we can rely on these graphs to compute …

• Verifying the Forward Analysis

  5259 words, about 25 minutes to read.

  In the previous post, we put together a number of powerful pieces of machinery to construct a sign analysis. However, we still haven’t verified that this analysis produces …