Symbolic algorithms for solving games of infinite duration.
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.
Python interface to Graphviz's Dot
Parser and abstract syntax tree for the Promela modeling language.
Python tools for working with TLA+ specifications.
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.