Implementing and Verifying "Static Program Analysis" in Agda
Series status: Ongoing
First post in 2024, last post in 2024
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
862 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) “abovebelow” lattice, which modified an arbitrary set with “bottom” and “top” elements ($\bot$ and $\top$ respectively). ...

Lattices of Finite Height
7169 words, about 34 minutes to read.
In the previous post, I introduced the class of finiteheight lattices: lattices where chains made from elements and the lessthan operator < can only be so long. ...

The FixedPoint 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 use of these lattices; this algorithm will be at the core of this series. ...

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