MAF2 is the successor of MAF a framework for experimenting with modular static analyses that are based on abstract interpretation. This iteration of the framework focusses on monadic implementations of the so-called "Abstracting Definitional Interpreters" (Darais et al., 2017) technique to static analysis.
The previous version of MAF focussed on static analyses developed according to the ModX technique. While this current iteration of the framwork still includes an implementation of the algorithms used in this ModX technique, its analyses are not structured in this way. Rather, ModX is viewed as an intelligent worklist algorithm provided as a parameter to the analysis' implementation.
This section is a work in progress
The framework can be used in a standalone mode by interacting with it through a command line interface. This command line interface currently offers some basic analyses for Scheme and some utilities for testing parsing of Python programs. This CLI is offered by the maf2-analysis package, and can be executed by running stack run in this package.
Alternatively, the repository can be used as a set of libraries. This usage is illustrated by this repository, which implements a simple analysis for the extended lambda calculus. It also contains a suitable stack configuration to load our set of libraries from this repository through Github's infrastructure.
The project is structured as a monorepository containing several indepent libraries. The idea behind this structure is to enable re-use of each of the components in our framework, allowing them to be easily used in smaller experiments. The libraries that make up our framework are as follows:
maf2-domains: this library contains some core abstract domains that are used in our analyses. These abstract domains are underpinned by abstract interpretation theory and are formulated in terms of mathematical lattices.maf2-syntax: this library contains syntax parsing and preprocessing facilities for all targets of our analyses. Our analyses currently target Scheme and Python.maf2-analysis: this library contains our analyses.
Each library contains additional documentation about their structure and usage in third-party libraries/applications.
The original idea behind ModX comes from the following work on modular analysis: Effect-Driven Flow Analysis, and A general method for rendering static analyses for diverse concurrency models modular.
The previous iteration of the MAF framework is presented in the following publication:
- MAF: A Framework for Modular Static Analysis of Higher-Order Languages. SCAM
2020. pdf. See release:
SCAM 2020
MAF is a complete rework of the Scala-AM framework, which was not focused on modular static analysis but was primarily used to experiment with AAM-style analyses. An AAM implementation (inspired by Scala-AM) is provided in MAF for benchmarks comparisons. Scala-AM is described in the following publications:
- Scala-AM: A Modular Static Analysis Framework. SCAM 2016. pdf , doi.
- Building a Modular Static Analysis Framework in Scala. Scala@SPLASH 2016. pdf , doi.
MAF has been used for evaluating modular static analysis approaches in the following publications:
- A Parallel Worklist Algorithm and Its Exploration Heuristics for Static Modular Analyses. Journal of Systems and Software, Volume 181. 2021. pdf, doi.
- A Parallel Worklist Algorithm for Modular Analyses. SCAM
2020. pdf. See release:
SCAM 2020 - Incremental Flow Analysis through Computational Dependency Reification. SCAM
2020. pdf. _See release:
SCAM 2020 - Summary-Based Compositional Analysis for Soft Contract Verification. SCAM 2022. preprint pdf. git. artifact .
Scala-AM has been used for evaluating static analysis approaches in the following publications:
- Garbage-Free Abstract Interpretation through Abstract Reference Counting. ECOOP 2019. pdf.
- A general method for rendering static analyses for diverse concurrency models modular. Journal of Systems and Software, Volume 149. 2019. pdf, doi.
- Mailbox Abstractions for Static Analysis of Actor Programs. ECOOP 2017. pdf, doi.
- Employing Run-time Static Analysis to Improve Concolic Execution. BENEVOL 2017. pdf.
- Incrementalizing Abstract Interpretation. BENEVOL 2017. pdf.
- Static taint analysis of event-driven scheme programs. ELS 2017. pdf.
- Improving trace-based JIT optimisation using whole-program information. VMIL@SPLASH 2016. pdf, doi.
- STRAF: A Scala Framework for Experiments in Trace-Based JIT Compilation. GTTSE 2015. pdf, doi.
All code in this repository is licensed according to the license provided in the LICENSE file.