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.
Binary decision diagrams implemented in pure Python, as well as Cython wrappers of CUDD, Sylvan, and BuDDy.
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.