This tool analyzes context-free grammars w.r.t. certain undecidable problems like language universality,
inclusion, equivalence, intersection, and ambiguity. It uses an incremental SAT solver (so far: zChaff)
to scan regions of words of bounded length for witnesses resp. counterexamples. This results in a
semi-decision procedure, not an approximation. Hence, the results are sound and complete (for the bounds)
but the analysis may not terminate.
The current version is beta release only. No warranty can be given. Source code
can be downloaded here. It is distributed under the
BSD
license.
The program is written in
OCaml. You
will therefore need an OCaml compiler to produce the executables. We
recommend version ≥ 3.09, but smaller versions may also suffice. You
will also need the SAT solver
zChaff.
Again, we recommend version 2007.3.12.
If you want to be notified whenever a newer version is available
please provide your details. Otherwise leave the fields blank.
For installation instructions see the included README file.
Once installed type bin/cfganalyzer --help for a short usage guide.
A set of benchmark examples is provided in this TAR.GZ archive.