1. tarball for a satisfiability checker for propositional dynamic logic with converse written in Ocaml.