Software: LTL2AUT
Author(s): Marco Daniele
Documentation: available in the package
Description: LTL2AUT generates Buchi automata from LTL formulas. The software is also described in the CAV 1999 paper by Marco Daniele, Fausto Giunchiglia, and Moshe Y. Vardi.
Software: KBDD
Author(s): Guoqiang Pan
Documentation: available in the package
Description: BDD-based satisfiability solver for modal logic K. The software is also described in the CADE 2002 paper by Guoqiang Pan, Ulrike Sattler, and Moshe Y. Vardi and the CADE 2003 paper by Guoqiang Pan and Moshe Y. Vardi.
Software: QMRes
Author(s): Guoqiang Pan (See comments)
Comments: Multi-resolution with ZDDs implementation copyright Laurent Simon (homepage) used under permission.  Graph Library copyright Andrew Ladd (homepage) used under permission download here (This version is modified to include vertex ordering heuristics).  Download binary only for QMRes here.
Description: ZDD-based multi-resolution solver for QBF.  The software is also described in the CP 2004 paper by Guoqiang Pan and Moshe Y. Vardi.