Binary decision diagrams implemented in pure Python, as well as Cython wrappers of CUDD, Sylvan, and BuDDy.
Parser and abstract syntax tree for the Promela modeling language.
Symbolic algorithms for solving games of infinite duration.
Python interface to Graphviz's Dot
Python tools for working with TLA+ specifications.
Utilities for abstract syntax trees and parsing with PLY.
Create C call graphs from multiple source files using Cflow, producing linked PDF.
Parser and abstract syntax tree for the temporal logic of actions TLA+.
Generalized reactive(1) synthesis from Promela specifications.