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