@ -2,7 +2,8 @@
title: "Implementing and Verifying \"Static Program Analysis\" in Agda, Part 0: Intro"
series: "Static Program Analysis in Agda"
description: "In this post, I give a top-level overview of my work on formally verified static analyses"
date: 2024-07-06T17:37:42-07:00
date: 2024-05-30T19:36:58-07:00
draft: true
tags: ["Agda", "Programming Languages"]
---
@ -44,13 +45,13 @@ I'd like to cover the following major topics, spending a couple of posts on each
lattice-based static program analysis, the various elements of the
lattice represent different facts or properties that we know about the
program in question; operations on the lattice help us combine these facts
and reason about them. I write about this in {{< draftlink " Part 1: Lattices " " 01_spa_agda_lattices " > }} .
and reason about them. I write about this in [Part 1: Lattices ]({{< relref "01_spa_agda_lattices" >}} ) .
Interestingly, lattices can be made by combining other lattices in certain
ways. We can therefore use simpler lattices as building blocks to create
more complex ones, all while preserving the algebraic structure that
we need for program analysis. I write about this in
{{< draftlink " Part 2: Combining Lattices " " 02_spa_agda_combining_lattices " > }} .
[Part 2: Combining Lattices ]({{< relref "02_spa_agda_combining_lattices" >}} ) .
* __The Fixed-Point Algorithm__ : to analyze a program, we use information
that we already know to compute additional information. For instance,
@ -64,15 +65,9 @@ I'd like to cover the following major topics, spending a couple of posts on each
What does it mean for the output to stop changing? Roughly, that's when
the following equation holds: `knownInfo = analyze(knownInfo)` . In mathematics,
this is known as a [fixed point ](https://mathworld.wolfram.com/FixedPoint.html ).
To enable computing fixed points, we focus on a specific kind of lattices:
those with a _fixed height_ . I talk about what this means in
{{< draftlink " Part 3: Lattices of Finite Height " " 03_spa_agda_fixed_height " > }}.
Even if we restrict our attention to lattices of fixed height,
not all functions have fixed points; however, certain types of functions on
lattices always do. The _fixed-point algorithm_ is a way to compute these
points, and we will use this to drive our analyses. I talk
about this in {{< draftlink " Part 4: The Fixed-Point Algorithm " " 04_spa_agda_fixedpoint " > }}.
Crucially, not all functions have fixed points; however, certain types of
functions on lattices do. The fixed-point algorithm is a way to compute these
points, and we will use this to drive our analyses.
* __Correctness__ : putting together the work on lattices and the fixed-point
algorithm, we can implement a static program analyzer in Agda. However,
@ -94,6 +89,5 @@ I'd like to cover the following major topics, spending a couple of posts on each
### Navigation
Here are the posts that I’
* {{< draftlink " Lattices " " 01_spa_agda_lattices " > }}
* {{< draftlink " Combining Lattices " " 02_spa_agda_combining_lattices " > }}
* {{< draftlink " Lattices of Finite Height " " 03_spa_agda_fixed_height " > }}
* [Lattices ]({{< relref "01_spa_agda_lattices" >}} )
* [Combining Lattices ]({{< relref "02_spa_agda_combining_lattices" >}} )