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 in Agda. The goal is to have a formally verified, yet executable, static analyzer for a simple language.

• Intro

  870 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. ...

• 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 numbers, and the (parameterized) “above-below” lattice, which modified an arbitrary set with “bottom” and “top” elements ($\bot$ and $\top$ respectively). ...

• Lattices of Finite Height

  7168 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. ...