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 11/03/2010. It contains a minor bugfix compared to the first version 03/12/2007
(thanks to Paul Giannaros for pointing that out) in the transformation of CFGs into the required normal
form. 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. You want to unpack the archive
in a separate directory.
Once installed type bin/cfganalyzer --help for a short usage guide.
A set of benchmark examples is provided in this TAR.GZ archive.