Skip to content
ilyasergey edited this page Mar 13, 2012 · 12 revisions

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 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 pushdown system.

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

How to build

Execute

ant

from the project root. It will build the project and make an executable JAR archive at ./artifacts, given the Ant build tool and Java SDK are installed.

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 located at ./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, given a Scala runtime installed:

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 in the project root.

License

The sources are released under CRAPL license.

If you have questions or concerns about the CRAPL, or you need more information about this license, please contact Prof. Matthew Might.

Clone this wiki locally