Home

This is the Github project page for a experimental implementation of k-CFA and Pushdown k-CFA with optional Abstract Garbage Collection for a subset of Scheme programming language. The analysis is developed by as a systematic abstraction of a small-step CESK semantics for extended lambda-calculus in A-normal form.

Two different abstractions are supported: traditional polyvariant k-CFA with store-allocated continuations and a CFA2-model, based on the introspective pushdowns system.

All of this is the topic of an ICFP 2012 submission titled "Introspective Pushdown Analysis of Higher-order Programs".

How to run:

for a compiled project

scala -cp ./out/production/reachability org.ucombinator.scheme.cfa.RunCFA [options] fileName

for an executable jar with Scala SDK included ./artifacts

java -jar artifacts/GenericCFAForScheme.jar [options] fileName

if you need the help message:

java -jar artifacts/GenericCFAForScheme.jar

for an executable jar with NO Scala SDK included scala -cp GenericCFAForScheme.jar org.ucombinator.scheme.cfa.RunCFA [options] fileName

Implementation insights

Grep for the tag (REMARK) in the code for some non-obvious insights.

Examples

For example programs look at the folder benchmarks of the project.

License

The sources are released under CRAPL license (see http://matt.might.net/articles/crapl/).

If you have questions or concerns about the CRAPL, or you need more information about this license, please contact Prof. Matthew Might (http://matt.might.net/).