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 license.
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-2007-12-03.tgz. 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.

Martin Lange
Last modified: Thu Mar 11 17:16:20 CET 2010