TTT2

I am one of the main developers of the Tyrolean Termination Tool 2 (TTT2), a termination prover for term rewrite systems. Visit the tool on its own site.

CSI

I am one of the main developers of the confluence prover CSI. Visit the tool on its own site.

CaT

I am one of the main developers of the complexity prover CaT. Visit the tool on its own site.

MiniSmt

I am the main developer of MiniSmt, an SMT solver for non-linear (ir)rational arithmetic. Visit the tool on its own site.

IsaFor/CeTA

I formalized looping nontermination and decreasing diagrams in IsaFoR, a formalization of rewriting in the theorem prover Isabelle/HOL. Visit IsaFoR/CeTA on its own site.

KBCV

I have conceived the Knuth-Bendix Completion Visualizer, an interactive tool for Knuth-Bendix completion. Visit KBCV on its own site.