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