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 and for LambdaJS -- a core calculus for JavaScript. The analyses is developed by a systematic abstraction of a small-step CESK semantics.
For Scheme, two different abstractions are supported: traditional polyvariant k-CFA with store-allocated continuations and a CFA2-model, based on the introspective pushdown system. For LambdaJS, only pushdown-based analysis is implemented.
An implementation of a pushdown analysis with abstract garbage collection for Scheme is the topic of an ICFP 2012 paper titled "Introspective Pushdown Analysis of Higher-Order Programs".
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.
for a compiled project
scala -cp ./out/production/reachability org.ucombinator.cfa.RunCFA [options] fileName
for an executable jar with Scala SDK included located at ./artifacts
java -jar artifacts/GenericCFA.jar org.ucombinator.cfa.RunCFA [options] fileName
if you need the help message:
java -jar artifacts/GenericCFA.jar
for an executable jar with NO Scala SDK included, given a Scala runtime installed:
scala -cp artifacts/GenericCFANoScala.jar org.ucombinator.cfa.RunCFA [options] fileName
Grep for the tag (REMARK) in the code for some non-obvious insights.
For example programs look at the folder benchmarks in the project root.
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.