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, MiniSAT or PicoSAT)
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 first version was released on 03/12/2007. The second version was released on 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. The latest version was released on 26/12/2012. It contains a bugfix in the translation of
CFG rules of the form A -> A B or A -> B A when B can derive the empty word. (Thanks to Carles Creus for pointing that out.)
It is also the first version that can be used with MiniSAT and PicoSAT.
No warranty can be given. The source code can be downloaded by pressing the button below. CFGAnalyzer is distributed under the BSD
The program is written in OCaml. You
will therefore need an OCaml compiler to produce the executables. We
recommend a version ≥ 3.12.1, but smaller versions may also suffice. You
will also need any of the following SAT solvers.
CFGAnalyzer is avalailable as a TGZ-archive: cfganalyzer-2012-12-26.tgz
For installation instructions see the included README
Once installed type bin/cfganalyzer --help
for a short usage guide.
A set of benchmark examples is provided in this TAR.GZ archive
Last modified: Thu Mar 11 17:16:20 CET 2010